let D be set ; :: thesis: for f1, f2 being double-one-to-one FinSequence of D * st Values f1 misses Values f2 holds
f1 ^ f2 is double-one-to-one
let f1, f2 be double-one-to-one FinSequence of D * ; :: thesis: ( Values f1 misses Values f2 implies f1 ^ f2 is double-one-to-one )
assume A1: Values f1 misses Values f2 ; :: thesis: f1 ^ f2 is double-one-to-one
set F = f1 ^ f2;
let x1, x2, y1, y2 be object ; :: according to FLEXARY1:def 6 :: thesis: ( x1 in dom (f1 ^ f2) & y1 in dom ((f1 ^ f2) . x1) & x2 in dom (f1 ^ f2) & y2 in dom ((f1 ^ f2) . x2) & (f1 ^ f2) _ (x1,y1) = (f1 ^ f2) _ (x2,y2) implies ( x1 = x2 & y1 = y2 ) )
assume A2: ( x1 in dom (f1 ^ f2) & y1 in dom ((f1 ^ f2) . x1) & x2 in dom (f1 ^ f2) & y2 in dom ((f1 ^ f2) . x2) & (f1 ^ f2) _ (x1,y1) = (f1 ^ f2) _ (x2,y2) ) ; :: thesis: ( x1 = x2 & y1 = y2 )
reconsider x1 = x1, x2 = x2 as Nat by A2;

per cases ( ( x1 in dom f1 & x2 in dom f1 ) or ( x1 in dom f1 & not x2 in dom f1 ) or ( not x1 in dom f1 & x2 in dom f1 ) or ( not x1 in dom f1 & not x2 in dom f1 ) ) ;

suppose A3: ( x1 in dom f1 & x2 in dom f1 ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then A4: ( (f1 ^ f2) . x1 = f1 . x1 & (f1 ^ f2) . x2 = f1 . x2 ) by FINSEQ_1:def 7;
then f1 _ (x1,y1) = f1 _ (x2,y2) by A2;
hence ( x1 = x2 & y1 = y2 ) by A2, A3, Def6, A4; :: thesis: verum

end;

suppose A5: ( x1 in dom f1 & not x2 in dom f1 ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then consider n being Nat such that
A6: ( n in dom f2 & x2 = (len f1) + n ) by A2, FINSEQ_1:25;
( (f1 ^ f2) . x2 = f2 . n & (f1 ^ f2) . x1 = f1 . x1 ) by A5, A6, FINSEQ_1:def 7;
then ( ((f1 ^ f2) . x2) . y2 in Values f2 & ((f1 ^ f2) . x2) . y2 in Values f1 ) by A2, A5, A6, Th1;
hence ( x1 = x2 & y1 = y2 ) by A1, XBOOLE_0:3; :: thesis: verum

end;

suppose A7: ( not x1 in dom f1 & x2 in dom f1 ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then consider n being Nat such that
A8: ( n in dom f2 & x1 = (len f1) + n ) by A2, FINSEQ_1:25;
( (f1 ^ f2) . x1 = f2 . n & (f1 ^ f2) . x2 = f1 . x2 ) by A7, A8, FINSEQ_1:def 7;
then ( ((f1 ^ f2) . x2) . y2 in Values f1 & ((f1 ^ f2) . x2) . y2 in Values f2 ) by A2, A7, A8, Th1;
hence ( x1 = x2 & y1 = y2 ) by A1, XBOOLE_0:3; :: thesis: verum

end;

suppose A9: ( not x1 in dom f1 & not x2 in dom f1 ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then consider n being Nat such that
A10: ( n in dom f2 & x1 = (len f1) + n ) by A2, FINSEQ_1:25;
consider k being Nat such that
A11: ( k in dom f2 & x2 = (len f1) + k ) by A2, A9, FINSEQ_1:25;
A12: ( (f1 ^ f2) . x1 = f2 . n & (f1 ^ f2) . x2 = f2 . k ) by A10, A11, FINSEQ_1:def 7;
then f2 _ (n,y1) = f2 _ (k,y2) by A2;
hence ( x1 = x2 & y1 = y2 ) by A2, A10, A11, Def6, A12; :: thesis: verum

end;

end;