let m, n1, n2, k be non zero Nat; :: thesis: for X being non-empty m -element FinSequence st k <= n1 & n1 <= n2 & n2 <= m holds
(Pt2FinSeq (SubFin (X,n1))) . k = (Pt2FinSeq (SubFin (X,n2))) . k
let X be non-empty m -element FinSequence; :: thesis: ( k <= n1 & n1 <= n2 & n2 <= m implies (Pt2FinSeq (SubFin (X,n1))) . k = (Pt2FinSeq (SubFin (X,n2))) . k )
assume that
A1: k <= n1 and
A2: n1 <= n2 and
A3: n2 <= m ; :: thesis: (Pt2FinSeq (SubFin (X,n1))) . k = (Pt2FinSeq (SubFin (X,n2))) . k
set X1 = SubFin (X,n1);
set X2 = SubFin (X,n2);
defpred S1[ Nat] means ( 1 <= $1 & $1 <= n1 implies ex i being non zero Nat st
( i = $1 & (Pt2FinSeq (SubFin (X,n1))) . i = (Pt2FinSeq (SubFin (X,n2))) . i ) );
A4: S1[ 0 ] ;
A5: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A6: S1[i] ; :: thesis: S1[i + 1]
assume A7: ( 1 <= i + 1 & i + 1 <= n1 ) ; :: thesis: ex i being non zero Nat st
( i = i + 1 & (Pt2FinSeq (SubFin (X,n1))) . i = (Pt2FinSeq (SubFin (X,n2))) . i )
reconsider i1 = i + 1 as non zero Nat ;
take i1 ; :: thesis: ( i1 = i + 1 & (Pt2FinSeq (SubFin (X,n1))) . i1 = (Pt2FinSeq (SubFin (X,n2))) . i1 )
thus i1 = i + 1 ; :: thesis: (Pt2FinSeq (SubFin (X,n1))) . i1 = (Pt2FinSeq (SubFin (X,n2))) . i1
thus (Pt2FinSeq (SubFin (X,n1))) . i1 = (Pt2FinSeq (SubFin (X,n2))) . i1 :: thesis: verum
proof
per cases ( i = 0 or i <> 0 ) ;
suppose A8: i = 0 ; :: thesis: (Pt2FinSeq (SubFin (X,n1))) . i1 = (Pt2FinSeq (SubFin (X,n2))) . i1
consider id1 being Function of (CarProduct (SubFin ((SubFin (X,n1)),1))),(product (SubFin ((SubFin (X,n1)),1))) such that
A9: ( (Pt2FinSeq (SubFin (X,n1))) . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin ((SubFin (X,n1)),1)) holds
id1 . x = <*x*> ) ) by Def5;
consider id2 being Function of (CarProduct (SubFin ((SubFin (X,n2)),1))),(product (SubFin ((SubFin (X,n2)),1))) such that
A10: ( (Pt2FinSeq (SubFin (X,n2))) . 1 = id2 & id2 is bijective & ( for x being object st x in CarProduct (SubFin ((SubFin (X,n2)),1)) holds
id2 . x = <*x*> ) ) by Def5;
A11: ( dom id1 = CarProduct (SubFin ((SubFin (X,n1)),1)) & dom id2 = CarProduct (SubFin ((SubFin (X,n2)),1)) ) by FUNCT_2:def 1;
1 <= n1 by NAT_1:14;
then A12: SubFin ((SubFin (X,n1)),1) = SubFin ((SubFin (X,n2)),1) by A2, A3, Th8;
for x being object st x in dom id1 holds
id1 . x = id2 . x
proof
let x be object ; :: thesis: ( x in dom id1 implies id1 . x = id2 . x )
assume A13: x in dom id1 ; :: thesis: id1 . x = id2 . x
then id1 . x = <*x*> by A9;
hence id1 . x = id2 . x by A12, A10, A13; :: thesis: verum
end;
hence (Pt2FinSeq (SubFin (X,n1))) . i1 = (Pt2FinSeq (SubFin (X,n2))) . i1 by A8, A12, A9, A10, A11, FUNCT_1:2; :: thesis: verum
end;
suppose i <> 0 ; :: thesis: (Pt2FinSeq (SubFin (X,n1))) . i1 = (Pt2FinSeq (SubFin (X,n2))) . i1
then consider i0 being non zero Nat such that
A14: ( i0 = i & (Pt2FinSeq (SubFin (X,n1))) . i0 = (Pt2FinSeq (SubFin (X,n2))) . i0 ) by A6, A7, NAT_1:13, NAT_1:14;
A15: i < n1 by A7, NAT_1:13;
then consider F1 being Function of (CarProduct (SubFin ((SubFin (X,n1)),i0))),(product (SubFin ((SubFin (X,n1)),i0))), I1 being Function of [:(CarProduct (SubFin ((SubFin (X,n1)),i0))),(ElmFin ((SubFin (X,n1)),(i0 + 1))):],(product (SubFin ((SubFin (X,n1)),(i0 + 1)))) such that
A16: ( F1 = (Pt2FinSeq (SubFin (X,n1))) . i0 & I1 = (Pt2FinSeq (SubFin (X,n1))) . (i0 + 1) & F1 is bijective & I1 is bijective & ( for x, y being object st x in CarProduct (SubFin ((SubFin (X,n1)),i0)) & y in ElmFin ((SubFin (X,n1)),(i0 + 1)) holds
ex s being FinSequence st
( F1 . x = s & I1 . (x,y) = s ^ <*y*> ) ) ) by A14, Def5;
i < n2 by A15, A2, XXREAL_0:2;
then consider F2 being Function of (CarProduct (SubFin ((SubFin (X,n2)),i0))),(product (SubFin ((SubFin (X,n2)),i0))), I2 being Function of [:(CarProduct (SubFin ((SubFin (X,n2)),i0))),(ElmFin ((SubFin (X,n2)),(i0 + 1))):],(product (SubFin ((SubFin (X,n2)),(i0 + 1)))) such that
A17: ( F2 = (Pt2FinSeq (SubFin (X,n2))) . i0 & I2 = (Pt2FinSeq (SubFin (X,n2))) . (i0 + 1) & F2 is bijective & I2 is bijective & ( for x, y being object st x in CarProduct (SubFin ((SubFin (X,n2)),i0)) & y in ElmFin ((SubFin (X,n2)),(i0 + 1)) holds
ex s being FinSequence st
( F2 . x = s & I2 . (x,y) = s ^ <*y*> ) ) ) by A14, Def5;
A18: ( SubFin ((SubFin (X,n1)),i0) = SubFin ((SubFin (X,n2)),i0) & ElmFin ((SubFin (X,n1)),(i0 + 1)) = ElmFin ((SubFin (X,n2)),(i0 + 1)) ) by A7, A15, A14, A2, A3, Th8;
A19: ( dom I1 = [:(CarProduct (SubFin ((SubFin (X,n1)),i0))),(ElmFin ((SubFin (X,n1)),(i0 + 1))):] & dom I2 = [:(CarProduct (SubFin ((SubFin (X,n2)),i0))),(ElmFin ((SubFin (X,n2)),(i0 + 1))):] ) by FUNCT_2:def 1;
for z being object st z in dom I1 holds
I1 . z = I2 . z
proof
let z be object ; :: thesis: ( z in dom I1 implies I1 . z = I2 . z )
assume z in dom I1 ; :: thesis: I1 . z = I2 . z
then consider x, y being object such that
A20: ( x in CarProduct (SubFin ((SubFin (X,n1)),i0)) & y in ElmFin ((SubFin (X,n1)),(i0 + 1)) & z = [x,y] ) by ZFMISC_1:84;
A21: ex s1 being FinSequence st
( F1 . x = s1 & I1 . (x,y) = s1 ^ <*y*> ) by A16, A20;
ex s2 being FinSequence st
( F2 . x = s2 & I2 . (x,y) = s2 ^ <*y*> ) by A18, A20, A17;
hence I1 . z = I2 . z by A14, A16, A17, A20, A21; :: thesis: verum
end;
then I1 = I2 by A18, A19;
hence (Pt2FinSeq (SubFin (X,n1))) . i1 = (Pt2FinSeq (SubFin (X,n2))) . i1 by A14, A16, A17; :: thesis: verum
end;
end;
end;
end;
A22: for i being Nat holds S1[i] from NAT_1:sch 2(A4, A5);
 1 <= k by NAT_1:14;
then ex i being non zero Nat st
( i = k & (Pt2FinSeq (SubFin (X,n1))) . i = (Pt2FinSeq (SubFin (X,n2))) . i ) by A1, A22;
hence (Pt2FinSeq (SubFin (X,n1))) . k = (Pt2FinSeq (SubFin (X,n2))) . k ; :: thesis: verum