let n be non zero Nat; :: thesis: for X being non-empty n + 1 -element FinSequence
for x, y being object st x in CarProduct (SubFin (X,n)) & y in ElmFin (X,(n + 1)) holds
ex s, t being FinSequence st
( (CarProd (SubFin (X,n))) . x = s & <*y*> = t & (CarProd X) . (x,y) = s ^ t )
let X be non-empty n + 1 -element FinSequence; :: thesis: for x, y being object st x in CarProduct (SubFin (X,n)) & y in ElmFin (X,(n + 1)) holds
ex s, t being FinSequence st
( (CarProd (SubFin (X,n))) . x = s & <*y*> = t & (CarProd X) . (x,y) = s ^ t )
let x, y be object ; :: thesis: ( x in CarProduct (SubFin (X,n)) & y in ElmFin (X,(n + 1)) implies ex s, t being FinSequence st
( (CarProd (SubFin (X,n))) . x = s & <*y*> = t & (CarProd X) . (x,y) = s ^ t ) )
assume A1: ( x in CarProduct (SubFin (X,n)) & y in ElmFin (X,(n + 1)) ) ; :: thesis: ex s, t being FinSequence st
( (CarProd (SubFin (X,n))) . x = s & <*y*> = t & (CarProd X) . (x,y) = s ^ t )
A2: n < n + 1 by NAT_1:13;
then consider F being Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n))), G being Function of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],(product (SubFin (X,(n + 1)))) such that
A3: ( F = (Pt2FinSeq X) . n & G = (Pt2FinSeq X) . (n + 1) & F is bijective & G is bijective & ( for x, y being object st x in CarProduct (SubFin (X,n)) & y in ElmFin (X,(n + 1)) holds
ex s being FinSequence st
( F . x = s & G . (x,y) = s ^ <*y*> ) ) ) by Def5;
consider s being FinSequence such that
A4: ( F . x = s & G . (x,y) = s ^ <*y*> ) by A1, A3;
set t = <*y*>;
take s ; :: thesis: ex t being FinSequence st
( (CarProd (SubFin (X,n))) . x = s & <*y*> = t & (CarProd X) . (x,y) = s ^ t )
take <*y*> ; :: thesis: ( (CarProd (SubFin (X,n))) . x = s & <*y*> = <*y*> & (CarProd X) . (x,y) = s ^ <*y*> )
thus ( (CarProd (SubFin (X,n))) . x = s & <*y*> = <*y*> & (CarProd X) . (x,y) = s ^ <*y*> ) by A3, A4, A2, Th10; :: thesis: verum