defpred S_{1}[ 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)

_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A25, A2);

hence f . (Product (F1 |^ I)) = Product (F2 |^ I) by A1; :: thesis: verum

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_{1}[n] holds

S_{1}[n + 1]

A25:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

thus S_{1}[n + 1]
:: thesis: verum

end;assume A3: S

thus S

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;

.= 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;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)

A21: F2 . (n + 1) =
(F2n ^ <*h*>) . ((len F2n) + 1)
by A6, A7, A11, A16, FINSEQ_1:40
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;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

.= 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

proof

for n being Nat holds S
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 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

hence f . (Product (F1 |^ I)) = Product (F2 |^ I) by A1; :: thesis: verum