let G be Group; :: thesis: for a being Element of G
for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I)
let a be Element of G; :: thesis: for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I)
defpred S₁[ FinSequence of INT ] means Product (((len $1) |-> a) |^ $1) = a |^ (Sum $1);
A1: S₁[ <*> INT ] by Lm2;
A2: for p being FinSequence of INT
for x being Element of INT st S₁[p] holds
S₁[p ^ <*x*>] by Lm3;
for p being FinSequence of INT holds S₁[p] from FINSEQ_2:sch 2(A1, A2);
hence for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I) ; :: thesis: verum