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; 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; 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; 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 ; 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; ( ( 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 )
; f . (Product (F1 |^ I)) = Product (F2 |^ I)
A2:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A3:
S1[
n]
;
S1[n + 1]thus
S1[
n + 1]
verumproof
let G,
H be
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 & n + 1 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)let F1 be
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 F2 be
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 I be
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 f be
Homomorphism of
G,
H;
( ( 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)
;
( 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
;
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 for k being Nat st k in dom F1n holds
F2n . k = f . (F1n . k)let k be
Nat;
( 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
;
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
;
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;
verum
end; end;
A25:
S1[ 0 ]
proof
let G,
H be
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 & 0 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)let F1 be
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 F2 be
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 I be
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 f be
Homomorphism of
G,
H;
( ( 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)
;
( 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
;
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;
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; verum