let D be set ; 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 * ; ( Values f1 misses Values f2 implies f1 ^ f2 is double-one-to-one )
assume A1:
Values f1 misses Values f2
; f1 ^ f2 is double-one-to-one
set F = f1 ^ f2;
let x1, x2, y1, y2 be object ; FLEXARY1:def 6 ( 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) )
; ( 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 A9:
( not
x1 in dom f1 & not
x2 in dom f1 )
;
( 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;
verum end; end;