let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for P being Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n))) st n <= m & P = (Pt2FinSeq X) . n holds
P is bijective
let X be non-empty m -element FinSequence; :: thesis: for P being Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n))) st n <= m & P = (Pt2FinSeq X) . n holds
P is bijective
let P be Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n))); :: thesis: ( n <= m & P = (Pt2FinSeq X) . n implies P is bijective )
assume that
A1: n <= m and
A2: P = (Pt2FinSeq X) . n ; :: thesis: P is bijective
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= n implies ex i being non zero Nat ex F being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) st
( $1 = i & F = (Pt2FinSeq X) . i & F is bijective ) );
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 ex F being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) st
( k + 1 = i & F = (Pt2FinSeq X) . i & F is bijective )

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

suppose A7: k = 0 ; :: thesis: ex i being non zero Nat ex F being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) st
( k + 1 = i & F = (Pt2FinSeq X) . i & F is bijective )

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 ex i being non zero Nat ex F being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) st
( k + 1 = i & F = (Pt2FinSeq X) . i & F is bijective ) by A7; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: ex i being non zero Nat ex F being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) st
( k + 1 = i & F = (Pt2FinSeq X) . i & F is bijective )

then consider i0 being non zero Nat, F0 being Function of (CarProduct (SubFin (X,i0))),(product (SubFin (X,i0))) such that
A8: ( k = i0 & F0 = (Pt2FinSeq X) . i0 & F0 is bijective ) 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 F 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: ( F = (Pt2FinSeq X) . i0 & IK = (Pt2FinSeq X) . (i0 + 1) & F 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
( F . x = s & IK . (x,y) = s ^ <*y*> ) ) ) by Def5;
reconsider i = i0 + 1 as non zero Nat ;
CarProduct (SubFin (X,(i0 + 1))) = [:(CarProduct (SubFin (X,i0))),(ElmFin (X,(i0 + 1))):] by A9, MEASUR13:9;
then reconsider IK = IK as Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ;
take i ; :: thesis: ex F being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) st
( k + 1 = i & F = (Pt2FinSeq X) . i & F is bijective )
take IK ; :: thesis: ( k + 1 = i & IK = (Pt2FinSeq X) . i & IK is bijective )
thus ( k + 1 = i & IK = (Pt2FinSeq X) . i & IK is bijective ) by A8, A10; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
then S₁[n] ;
hence P is bijective by A2, NAT_1:14; :: thesis: verum