defpred S1[ Nat] means for G, H being Group
for F1 being FinSequence of the carrier of G
for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & \$1 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I);
let G, H be Group; :: thesis: for F1 being FinSequence of the carrier of G
for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let F1 be FinSequence of the carrier of G; :: thesis: for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let F2 be FinSequence of the carrier of H; :: thesis: for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let I be FinSequence of INT ; :: thesis: for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let f be Homomorphism of G,H; :: thesis: ( ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I implies f . (Product (F1 |^ I)) = Product (F2 |^ I) )

assume A1: ( ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I ) ; :: thesis: f . (Product (F1 |^ I)) = Product (F2 |^ I)
A2: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let G, H be Group; :: thesis: for F1 being FinSequence of the carrier of G
for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & n + 1 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let F1 be FinSequence of the carrier of G; :: thesis: for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & n + 1 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let F2 be FinSequence of the carrier of H; :: thesis: for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & n + 1 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let I be FinSequence of INT ; :: thesis: for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & n + 1 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let f be Homomorphism of G,H; :: thesis: ( ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & n + 1 = len I implies f . (Product (F1 |^ I)) = Product (F2 |^ I) )

assume A4: for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ; :: thesis: ( not len F1 = len I or not len F2 = len I or not n + 1 = len I or f . (Product (F1 |^ I)) = Product (F2 |^ I) )
assume that
A5: len F1 = len I and
A6: len F2 = len I and
A7: n + 1 = len I ; :: thesis: f . (Product (F1 |^ I)) = Product (F2 |^ I)
consider F1n being FinSequence of the carrier of G, g being Element of G such that
A8: F1 = F1n ^ <*g*> by ;
A9: len F1 = (len F1n) + () by ;
then A10: n + 1 = (len F1n) + 1 by ;
consider F2n being FinSequence of the carrier of H, h being Element of H such that
A11: F2 = F2n ^ <*h*> by ;
A12: ( dom F1 = dom F2 & dom F2 = dom I ) by ;
1 <= n + 1 by NAT_1:11;
then A13: n + 1 in dom I by ;
set F21 = <*h*>;
set F11 = <*g*>;
consider In being FinSequence of INT , i being Element of INT such that
A14: I = In ^ <*i*> by ;
set I1 = <*i*>;
len I = (len In) + () by ;
then A15: n + 1 = (len In) + 1 by ;
A16: len F2 = (len F2n) + () by ;
then A17: n + 1 = (len F2n) + 1 by ;
A18: now :: thesis: for k being Nat st k in dom F1n holds
F2n . k = f . (F1n . k)
let k be Nat; :: thesis: ( k in dom F1n implies F2n . k = f . (F1n . k) )
0 + n <= 1 + n by XREAL_1:6;
then A19: dom F1n c= dom F1 by ;
assume A20: k in dom F1n ; :: thesis: F2n . k = f . (F1n . k)
then k in dom F2n by ;
hence F2n . k = F2 . k by
.= f . (F1 . k) by A4, A20, A19
.= f . (F1n . k) by ;
:: thesis: verum
end;
A21: F2 . (n + 1) = (F2n ^ <*h*>) . ((len F2n) + 1) by
.= h by FINSEQ_1:42 ;
A22: F1 . (n + 1) = (F1n ^ <*g*>) . ((len F1n) + 1) by
.= g by FINSEQ_1:42 ;
len <*h*> = 1 by FINSEQ_1:40
.= len <*i*> by FINSEQ_1:40 ;
then A23: Product (F2 |^ I) = Product ((F2n |^ In) ^ ()) by
.= (Product (F2n |^ In)) * (Product ()) by GROUP_4:5 ;
A24: f . (Product ()) = f . (Product (<*g*> |^ <*(@ i)*>))
.= f . (Product <*(g |^ i)*>) by GROUP_4:22
.= f . (g |^ i) by GROUP_4:9
.= (f . g) |^ i by GROUP_6:37
.= h |^ i by A4, A13, A12, A22, A21
.= Product <*(h |^ i)*> by GROUP_4:9
.= Product (<*h*> |^ <*(@ i)*>) by GROUP_4:22
.= Product () ;
len <*g*> = 1 by FINSEQ_1:40
.= len <*i*> by FINSEQ_1:40 ;
then Product (F1 |^ I) = Product ((F1n |^ In) ^ ()) by
.= (Product (F1n |^ In)) * (Product ()) by GROUP_4:5 ;
then f . (Product (F1 |^ I)) = (f . (Product (F1n |^ In))) * (f . (Product ())) by GROUP_6:def 6
.= (Product (F2n |^ In)) * (Product ()) by A3, A15, A10, A17, A18, A24 ;
hence f . (Product (F1 |^ I)) = Product (F2 |^ I) by A23; :: thesis: verum
end;
end;
A25: S1[ 0 ]
proof
let G, H be Group; :: thesis: for F1 being FinSequence of the carrier of G
for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & 0 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let F1 be FinSequence of the carrier of G; :: thesis: for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & 0 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let F2 be FinSequence of the carrier of H; :: thesis: for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & 0 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let I be FinSequence of INT ; :: thesis: for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & 0 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

let f be Homomorphism of G,H; :: thesis: ( ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I & 0 = len I implies f . (Product (F1 |^ I)) = Product (F2 |^ I) )

assume for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ; :: thesis: ( not len F1 = len I or not len F2 = len I or not 0 = len I or f . (Product (F1 |^ I)) = Product (F2 |^ I) )
assume that
A26: len F1 = len I and
A27: len F2 = len I and
A28: 0 = len I ; :: thesis: f . (Product (F1 |^ I)) = Product (F2 |^ I)
len (F2 |^ I) = 0 by ;
then F2 |^ I = <*> the carrier of H ;
then A29: Product (F2 |^ I) = 1_ H by GROUP_4:8;
len (F1 |^ I) = 0 by ;
then F1 |^ I = <*> the carrier of G ;
then Product (F1 |^ I) = 1_ G by GROUP_4:8;
hence f . (Product (F1 |^ I)) = Product (F2 |^ I) by ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A25, A2);
hence f . (Product (F1 |^ I)) = Product (F2 |^ I) by A1; :: thesis: verum