defpred S₁[ 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 S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[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 A5, A7, FINSEQ_2:19;
A9: len F1 = (len F1n) + (len <*g*>) by A8, FINSEQ_1:22;
then A10: n + 1 = (len F1n) + 1 by A5, A7, FINSEQ_1:40;
consider F2n being FinSequence of the carrier of H, h being Element of H such that
A11: F2 = F2n ^ <*h*> by A6, A7, FINSEQ_2:19;
A12: ( dom F1 = dom F2 & dom F2 = dom I ) by A5, A6, FINSEQ_3:29;
1 <= n + 1 by NAT_1:11;
then A13: n + 1 in dom I by A7, FINSEQ_3:25;
set F21 = <*h*>;
set F11 = <*g*>;
consider In being FinSequence of INT , i being Element of INT such that
A14: I = In ^ <*i*> by A7, FINSEQ_2:19;
set I1 = <*i*>;
len I = (len In) + (len <*i*>) by A14, FINSEQ_1:22;
then A15: n + 1 = (len In) + 1 by A7, FINSEQ_1:40;
A16: len F2 = (len F2n) + (len <*h*>) by A11, FINSEQ_1:22;
then A17: n + 1 = (len F2n) + 1 by A6, A7, FINSEQ_1:40;

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 A5, A7, A10, FINSEQ_3:30;
assume A20: k in dom F1n ; :: thesis: F2n . k = f . (F1n . k)
then k in dom F2n by A10, A17, FINSEQ_3:29;
hence F2n . k = F2 . k by A11, FINSEQ_1:def 7
.= f . (F1 . k) by A4, A20, A19
.= f . (F1n . k) by A8, A20, FINSEQ_1:def 7 ;
:: thesis: verum

end;

A21: F2 . (n + 1) = (F2n ^ <*h*>) . ((len F2n) + 1) by A6, A7, A11, A16, FINSEQ_1:40
.= h by FINSEQ_1:42 ;
A22: F1 . (n + 1) = (F1n ^ <*g*>) . ((len F1n) + 1) by A5, A7, A8, A9, FINSEQ_1:40
.= 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) ^ (<*h*> |^ <*i*>)) by A14, A11, A15, A17, GROUP_4:19
.= (Product (F2n |^ In)) * (Product (<*h*> |^ <*i*>)) by GROUP_4:5 ;
A24: f . (Product (<*g*> |^ <*i*>)) = 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 (<*h*> |^ <*i*>) ;
len <*g*> = 1 by FINSEQ_1:40
.= len <*i*> by FINSEQ_1:40 ;
then Product (F1 |^ I) = Product ((F1n |^ In) ^ (<*g*> |^ <*i*>)) by A14, A8, A15, A10, GROUP_4:19
.= (Product (F1n |^ In)) * (Product (<*g*> |^ <*i*>)) by GROUP_4:5 ;
then f . (Product (F1 |^ I)) = (f . (Product (F1n |^ In))) * (f . (Product (<*g*> |^ <*i*>))) by GROUP_6:def 6
.= (Product (F2n |^ In)) * (Product (<*h*> |^ <*i*>)) by A3, A15, A10, A17, A18, A24 ;
hence f . (Product (F1 |^ I)) = Product (F2 |^ I) by A23; :: thesis: verum

end;

end;

A25: S₁[ 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 A27, A28, GROUP_4:def 3;
then F2 |^ I = <*> the carrier of H ;
then A29: Product (F2 |^ I) = 1_ H by GROUP_4:8;
len (F1 |^ I) = 0 by A26, A28, GROUP_4:def 3;
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 A29, GROUP_6:31; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A25, A2);
hence f . (Product (F1 |^ I)) = Product (F2 |^ I) by A1; :: thesis: verum