let S1, S2 be m -element FinSequence; :: thesis: ( ex id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) st
( S1 . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) & ( for i being non zero Nat st i < m holds
ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ex IK being Function of [:(CarProduct (SubFin (X,i))),(ElmFin (X,(i + 1))):],(product (SubFin (X,(i + 1)))) st
( Fi = S1 . i & IK = S1 . (i + 1) & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,i)) & y in ElmFin (X,(i + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) ) & ex id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) st
( S2 . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) & ( for i being non zero Nat st i < m holds
ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ex IK being Function of [:(CarProduct (SubFin (X,i))),(ElmFin (X,(i + 1))):],(product (SubFin (X,(i + 1)))) st
( Fi = S2 . i & IK = S2 . (i + 1) & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,i)) & y in ElmFin (X,(i + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) ) implies S1 = S2 )
assume that
A51: ( ex id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) st
( S1 . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) & ( for i being non zero Nat st i < m holds
ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ex IK being Function of [:(CarProduct (SubFin (X,i))),(ElmFin (X,(i + 1))):],(product (SubFin (X,(i + 1)))) st
( Fi = S1 . i & IK = S1 . (i + 1) & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,i)) & y in ElmFin (X,(i + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) ) ) and
A52: ( ex id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) st
( S2 . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) & ( for i being non zero Nat st i < m holds
ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ex IK being Function of [:(CarProduct (SubFin (X,i))),(ElmFin (X,(i + 1))):],(product (SubFin (X,(i + 1)))) st
( Fi = S2 . i & IK = S2 . (i + 1) & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,i)) & y in ElmFin (X,(i + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) ) ) ; :: thesis: S1 = S2
consider id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) such that
A53: ( S1 . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) by A51;
consider id2 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) such that
A54: ( S2 . 1 = id2 & id2 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id2 . x = <*x*> ) ) by A52;

A55: now :: thesis: for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = id2 . x

let x be object ; :: thesis: ( x in CarProduct (SubFin (X,1)) implies id1 . x = id2 . x )
assume A56: x in CarProduct (SubFin (X,1)) ; :: thesis: id1 . x = id2 . x
then id1 . x = <*x*> by A53;
hence id1 . x = id2 . x by A54, A56; :: thesis: verum

end;

defpred S₁[ Nat] means ( 1 <= $1 & $1 <= m implies S1 . $1 = S2 . $1 );
A57: S₁[ 0 ] ;
A58: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A59: S₁[i] ; :: thesis: S₁[i + 1]
assume A60: ( 1 <= i + 1 & i + 1 <= m ) ; :: thesis: S1 . (i + 1) = S2 . (i + 1)

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: S1 . (i + 1) = S2 . (i + 1)

hence S1 . (i + 1) = S2 . (i + 1) by A53, A54, A55, FUNCT_2:12; :: thesis: verum

end;

suppose A61: i <> 0 ; :: thesis: S1 . (i + 1) = S2 . (i + 1)

then i + 1 <> 1 ;
then A62: 1 < i + 1 by A60, XXREAL_0:1;
i + 0 < i + 1 by XREAL_1:8;
then A63: i < m by A60, XXREAL_0:2;
reconsider j = i as non zero Nat by A61;
consider Fi being Function of (CarProduct (SubFin (X,j))),(product (SubFin (X,j))), IK being Function of [:(CarProduct (SubFin (X,j))),(ElmFin (X,(j + 1))):],(product (SubFin (X,(j + 1)))) such that
A64: ( Fi = S1 . i & IK = S1 . (j + 1) & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,j)) & y in ElmFin (X,(j + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) by A51, A63;
consider Gi being Function of (CarProduct (SubFin (X,j))),(product (SubFin (X,j))), IL being Function of [:(CarProduct (SubFin (X,j))),(ElmFin (X,(j + 1))):],(product (SubFin (X,(i + 1)))) such that
A65: ( Gi = S2 . j & IL = S2 . (j + 1) & Gi is bijective & IL is bijective & ( for x, y being object st x in CarProduct (SubFin (X,j)) & y in ElmFin (X,(j + 1)) holds
ex s being FinSequence st
( Gi . x = s & IL . (x,y) = s ^ <*y*> ) ) ) by A52, A63;
for a being Element of CarProduct (SubFin (X,j))
for b being Element of ElmFin (X,(j + 1)) holds IK . (a,b) = IL . (a,b)

proof

let a be Element of CarProduct (SubFin (X,j)); :: thesis: for b being Element of ElmFin (X,(j + 1)) holds IK . (a,b) = IL . (a,b)
let b be Element of ElmFin (X,(j + 1)); :: thesis: IK . (a,b) = IL . (a,b)
A66: ex s being FinSequence st
( Fi . a = s & IK . (a,b) = s ^ <*b*> ) by A64;
ex s being FinSequence st
( Gi . a = s & IL . (a,b) = s ^ <*b*> ) by A65;
hence IK . (a,b) = IL . (a,b) by A66, A59, A62, A64, A65, A60, NAT_1:13; :: thesis: verum

end;

hence S1 . (i + 1) = S2 . (i + 1) by A64, A65, BINOP_1:2; :: thesis: verum

end;

end;

end;

A67: for i being Nat holds S₁[i] from NAT_1:sch 2(A57, A58);
( len S1 = m & len S2 = m ) by CARD_1:def 7;
hence S1 = S2 by A67; :: thesis: verum