# [isabelle] generalize a property

Dear all,
In Isabelle i always deal with simple algebra properties.
I
proved that having g,h,y,t in (G,times), (a, b, a1, b1, c, c1 :: int) and this two equations:
(g (^) a) times (h (^) b)= t times (y
(^) c)
and (g (^) a1) times (h (^) b1)= t times (y (^) c1)
==>(g (^) (a-a1)) times (h (^) (b-b1))= y (^) (c-c1) is true.
How can
i generalize this for finitely many base elements?
(for example to prove that
having (g1 (^) a1) times (g2 (^) a2) times... times (g87 (^) (a87))= t
times (y (^) c)
and (g1 (^) a1') times (g2 (^) a2') times... times (g87
(^) (a87'))= t times (y (^) c1)
to get true (g1 (^) (a1-a1')) times (g2
(^) (a2-a2')) times... times (g87 (^) (a87-a87')))= y (^) (c-c1)).
Is
there a way at all? Is is not right the way i look at the problem?
Thank you very much!
Stefania Barzan

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*