let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence st n <= m holds
(Pt2FinSeq X) . n is Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n)))
let X be non-empty m -element FinSequence; :: thesis: ( n <= m implies (Pt2FinSeq X) . n is Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n))) )
assume A1: n <= m ; :: thesis: (Pt2FinSeq X) . n is Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n)))
A2: 1 <= n by NAT_1:14;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= n implies ex i being non zero Nat st
( $1 = i & (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ) );
A3: S₁[ 0 ] ;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
assume A6: ( 1 <= k + 1 & k + 1 <= n ) ; :: thesis: ex i being non zero Nat st
( k + 1 = i & (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) )
reconsider i = k + 1 as non zero Nat ;
take i ; :: thesis: ( k + 1 = i & (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) )
thus k + 1 = i ; :: thesis: (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i)))
thus (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) :: thesis: verum

proof

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

suppose A7: k = 0 ; :: thesis: (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i)))

ex id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) st
( (Pt2FinSeq X) . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) by Def5;
hence (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) by A7; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i)))

then consider i0 being non zero Nat such that
A8: ( k = i0 & (Pt2FinSeq X) . i0 is Function of (CarProduct (SubFin (X,i0))),(product (SubFin (X,i0))) ) by A5, A6, NAT_1:13, NAT_1:14;
k < n by A6, NAT_1:13;
then A9: i0 < m by A1, A8, XXREAL_0:2;
then consider Fi being Function of (CarProduct (SubFin (X,i0))),(product (SubFin (X,i0))), IK being Function of [:(CarProduct (SubFin (X,i0))),(ElmFin (X,(i0 + 1))):],(product (SubFin (X,(i0 + 1)))) such that
A10: ( Fi = (Pt2FinSeq X) . i0 & IK = (Pt2FinSeq X) . (i0 + 1) & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,i0)) & y in ElmFin (X,(i0 + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) by Def5;
CarProduct (SubFin (X,(i0 + 1))) = [:(CarProduct (SubFin (X,i0))),(ElmFin (X,(i0 + 1))):] by A9, MEASUR13:9;
hence (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) by A8, A10; :: thesis: verum

end;

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
then consider i being non zero Nat such that
A11: ( i = n & (Pt2FinSeq X) . i is Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ) by A2;
thus (Pt2FinSeq X) . n is Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n))) by A11; :: thesis: verum