let G be Group; :: thesis: for F1, F2 being FinSequence of the carrier of G st len F1 = len F2 & ( for k being Nat st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) "
let F1, F2 be FinSequence of the carrier of G; :: thesis: ( len F1 = len F2 & ( for k being Nat st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
defpred S1[ Nat] means for F1, F2 being FinSequence of the carrier of G st len F1 = $1 & len F1 = len F2 & ( for k being Nat st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) " ;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
let F1, F2 be FinSequence of the carrier of G; :: thesis: ( len F1 = n + 1 & len F1 = len F2 & ( for k being Nat st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
assume that
A3: len F1 = n + 1 and
A4: len F1 = len F2 and
A5: for k being Nat st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ; :: thesis: Product F1 = (Product F2) "
reconsider p = F1 | (Seg n) as FinSequence of the carrier of G by FINSEQ_1:18;
deffunc H1( Nat) -> set = F2 . ($1 + 1);
consider q being FinSequence such that
A6: len q = len p and
A7: for k being Nat st k in dom q holds
q . k = H1(k) from FINSEQ_1:sch 2();
 A8: dom q = dom p by A6, FINSEQ_3:29;
A9: len p = n by A3, FINSEQ_3:53;
A10: rng q c= the carrier of G
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q or x in the carrier of G )
assume x in rng q ; :: thesis: x in the carrier of G
then consider y being object such that
A11: y in dom q and
A12: x = q . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A11;
y <= len p by A6, A11, FINSEQ_3:25;
then ( 1 <= y + 1 & y + 1 <= len F2 ) by A3, A4, A9, NAT_1:12, XREAL_1:7;
then A13: y + 1 in dom F2 by FINSEQ_3:25;
x = F2 . (y + 1) by A7, A11, A12;
then A14: x in rng F2 by A13, FUNCT_1:def 3;
rng F2 c= the carrier of G by FINSEQ_1:def 4;
hence x in the carrier of G by A14; :: thesis: verum
end;
A15: rng F1 c= the carrier of G by FINSEQ_1:def 4;
1 <= n + 1 by NAT_1:12;
then n + 1 in dom F1 by A3, FINSEQ_3:25;
then F1 . (n + 1) in rng F1 by FUNCT_1:def 3;
then reconsider a = F1 . (n + 1) as Element of G by A15;
A16: F1 = p ^ <*a*> by A3, FINSEQ_3:55;
A17: now :: thesis: for k being Nat st k in dom <*(a ")*> holds
<*(a ")*> . k = F2 . k
let k be Nat; :: thesis: ( k in dom <*(a ")*> implies <*(a ")*> . k = F2 . k )
assume k in dom <*(a ")*> ; :: thesis: <*(a ")*> . k = F2 . k
then A18: k in {1} by FINSEQ_1:2, FINSEQ_1:def 8;
len F2 >= 1 by A3, A4, NAT_1:12;
then A19: len F2 in dom F1 by A4, FINSEQ_3:25;
then F2 . (((len F1) - (len F1)) + 1) = (F1 /. (len F1)) " by A4, A5;
then (F1 /. (len F1)) " = F2 . k by A18, TARSKI:def 1;
then A20: F2 . k = a " by A3, A4, A19, PARTFUN1:def 6;
k = 1 by A18, TARSKI:def 1;
hence <*(a ")*> . k = F2 . k by A20, FINSEQ_1:def 8; :: thesis: verum
end;
reconsider q = q as FinSequence of the carrier of G by A10, FINSEQ_1:def 4;
now :: thesis: for k being Nat st k in dom p holds
q . (((len p) - k) + 1) = (p /. k) "
let k be Nat; :: thesis: ( k in dom p implies q . (((len p) - k) + 1) = (p /. k) " )
assume A21: k in dom p ; :: thesis: q . (((len p) - k) + 1) = (p /. k) "
then reconsider i = ((len p) - k) + 1 as Element of NAT by Lm3;
A22: i + 1 = ((len F1) - k) + 1 by A3, A9;
( 1 <= i & i <= len p ) by A21, Lm3;
then i in dom p by FINSEQ_3:25;
then A23: q . i = F2 . (i + 1) by A7, A8;
k <= len p by A21, FINSEQ_3:25;
then A24: k <= len F1 by A3, A9, NAT_1:12;
1 <= k by A21, FINSEQ_3:25;
then A25: k in dom F1 by A24, FINSEQ_3:25;
then F1 /. k = F1 . k by PARTFUN1:def 6
.= p . k by A21, FUNCT_1:47
.= p /. k by A21, PARTFUN1:def 6 ;
hence q . (((len p) - k) + 1) = (p /. k) " by A5, A23, A25, A22; :: thesis: verum
end;
then A26: Product p = (Product q) " by A2, A9, A6;
A27: now :: thesis: for k being Nat st k in dom q holds
F2 . ((len <*(a ")*>) + k) = q . k
let k be Nat; :: thesis: ( k in dom q implies F2 . ((len <*(a ")*>) + k) = q . k )
A28: len <*(a ")*> = 1 by FINSEQ_1:39;
assume k in dom q ; :: thesis: F2 . ((len <*(a ")*>) + k) = q . k
hence F2 . ((len <*(a ")*>) + k) = q . k by A7, A28; :: thesis: verum
end;
len F2 = (len <*(a ")*>) + (len q) by A3, A4, A9, A6, FINSEQ_1:39;
then F2 = <*(a ")*> ^ q by A17, A27, FINSEQ_3:38;
then Product F2 = (a ") * (Product q) by FINSOP_1:6
.= (a ") * ((Product p) ") by A26
.= ((Product p) * a) " by GROUP_1:17 ;
hence Product F1 = (Product F2) " by A16, FINSOP_1:4; :: thesis: verum
end;
A29: S1[ 0 ]
proof
let F1, F2 be FinSequence of the carrier of G; :: thesis: ( len F1 = 0 & len F1 = len F2 & ( for k being Nat st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
assume that
A30: len F1 = 0 and
A31: len F1 = len F2 ; :: thesis: ( ex k being Nat st
( k in dom F1 & not F2 . (((len F1) - k) + 1) = (F1 /. k) " ) or Product F1 = (Product F2) " )
F1 = <*> the carrier of G by A30;
then A32: Product F1 = 1_ G by Th8;
F2 = <*> the carrier of G by A30, A31;
then Product F2 = 1_ G by Th8;
hence ( ex k being Nat st
( k in dom F1 & not F2 . (((len F1) - k) + 1) = (F1 /. k) " ) or Product F1 = (Product F2) " ) by A32, GROUP_1:8; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A29, A1);
 hence ( len F1 = len F2 & ( for k being Nat st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " ) ; :: thesis: verum