let G be Group; :: thesis: for F1, F2 being FinSequence of the carrier of G st len F1 = len F2 & ( for k being Element of 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 Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
defpred S₁[ Element of NAT ] means for F1, F2 being FinSequence of the carrier of G st len F1 = $1 & len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) " ;
A1: S₁[ 0 ]

proof

let F1, F2 be FinSequence of the carrier of G; :: thesis: ( len F1 = 0 & len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
assume ( len F1 = 0 & len F1 = len F2 ) ; :: thesis: ( ex k being Element of NAT st
( k in dom F1 & not F2 . (((len F1) - k) + 1) = (F1 /. k) " ) or Product F1 = (Product F2) " )
then ( F1 = <*> the carrier of G & F2 = <*> the carrier of G ) ;
then ( Product F1 = 1_ G & Product F2 = 1_ G & 1_ G = (1_ G) " ) by Th11, GROUP_1:16;
hence ( ex k being Element of NAT st
( k in dom F1 & not F2 . (((len F1) - k) + 1) = (F1 /. k) " ) or Product F1 = (Product F2) " ) ; :: thesis: verum

end;

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let F1, F2 be FinSequence of the carrier of G; :: thesis: ( len F1 = n + 1 & len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
assume that
A4: ( len F1 = n + 1 & len F1 = len F2 ) and
A5: for k being Element of 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:23;
1 <= n + 1 by NAT_1:12;
then n + 1 in dom F1 by A4, FINSEQ_3:27;
then ( F1 . (n + 1) in rng F1 & rng F1 c= the carrier of G ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider a = F1 . (n + 1) as Element of G ;
A6: len p = n by A4, FINSEQ_3:59;
deffunc H₁( Nat) -> set = F2 . ($1 + 1);
consider q being FinSequence such that
A7: len q = len p and
A8: for k being Nat st k in dom q holds
q . k = H₁(k) from FINSEQ_1:sch 2();
A9: dom q = dom p by A7, FINSEQ_3:31;
rng q c= the carrier of G

proof

let x be set ; :: 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 set such that
A10: ( y in dom q & x = q . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A10;
A11: x = F2 . (y + 1) by A8, A10;
A12: 1 <= y + 1 by NAT_1:12;
y <= len p by A7, A10, FINSEQ_3:27;
then y + 1 <= len F2 by A4, A6, XREAL_1:9;
then y + 1 in dom F2 by A12, FINSEQ_3:27;
then ( x in rng F2 & rng F2 c= the carrier of G ) by A11, FINSEQ_1:def 4, FUNCT_1:def 5;
hence x in the carrier of G ; :: thesis: verum

end;

then reconsider q = q as FinSequence of the carrier of G by FINSEQ_1:def 4;
A13: len F2 = (len <*(a " )*>) + (len q) by A4, A6, A7, FINSEQ_1:56;

A14: now

let k be Element of NAT ; :: thesis: ( k in dom <*(a " )*> implies <*(a " )*> . k = F2 . k )
assume k in dom <*(a " )*> ; :: thesis: <*(a " )*> . k = F2 . k
then A15: k in {1} by FINSEQ_1:4, FINSEQ_1:def 8;
len F2 >= 1 by A4, NAT_1:12;
then A16: len F2 in dom F1 by A4, FINSEQ_3:27;
then F2 . (((len F1) - (len F1)) + 1) = (F1 /. (len F1)) " by A4, A5;
then (F1 /. (len F1)) " = F2 . k by A15, TARSKI:def 1;
then ( F2 . k = a " & k = 1 ) by A4, A15, A16, PARTFUN1:def 8, TARSKI:def 1;
hence <*(a " )*> . k = F2 . k by FINSEQ_1:def 8; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k in dom q implies F2 . ((len <*(a " )*>) + k) = q . k )
assume k in dom q ; :: thesis: F2 . ((len <*(a " )*>) + k) = q . k
then ( k in dom q & len <*(a " )*> = 1 & k + 1 = 1 + k ) by FINSEQ_1:56;
hence F2 . ((len <*(a " )*>) + k) = q . k by A8; :: thesis: verum

end;

then A17: F2 = <*(a " )*> ^ q by A13, A14, FINSEQ_3:43;

now

let k be Element of NAT ; :: thesis: ( k in dom p implies q . (((len p) - k) + 1) = (p /. k) " )
assume A18: 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;
( 1 <= i & i <= len p ) by A18, Lm3;
then i in dom p by FINSEQ_3:27;
then A19: q . i = F2 . (i + 1) by A8, A9;
( len p <= len F1 & k <= len p ) by A4, A6, A18, FINSEQ_3:27, NAT_1:12;
then ( 1 <= k & k <= len F1 ) by A18, FINSEQ_3:27, XXREAL_0:2;
then A20: k in dom F1 by FINSEQ_3:27;
A21: i + 1 = ((len F1) - k) + 1 by A4, A6;
F1 /. k = F1 . k by A20, PARTFUN1:def 8
.= p . k by A18, FUNCT_1:70
.= p /. k by A18, PARTFUN1:def 8 ;
hence q . (((len p) - k) + 1) = (p /. k) " by A5, A19, A20, A21; :: thesis: verum

end;

then A22: Product p = (Product q) " by A3, A6, A7;
F1 = p ^ <*a*> by A4, FINSEQ_3:61;
then A23: Product F1 = (Product p) * a by Th9;
Product F2 = (a " ) * (Product q) by A17, Th10
.= (a " ) * ((Product p) " ) by A22
.= ((Product p) * a) " by GROUP_1:25 ;
hence Product F1 = (Product F2) " by A23; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
hence ( len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " ) ; :: thesis: verum