let f be Function-yielding Function; :: thesis: ( f is double-one-to-one iff ( ( for x being object holds f . x is one-to-one ) & ( for x, y being object st x <> y holds
rng (f . x) misses rng (f . y) ) ) )
thus ( f is double-one-to-one implies ( ( for x being object holds f . x is one-to-one ) & ( for x, y being object st x <> y holds
rng (f . x) misses rng (f . y) ) ) ) :: thesis: ( ( for x being object holds f . x is one-to-one ) & ( for x, y being object st x <> y holds
rng (f . x) misses rng (f . y) ) implies f is double-one-to-one )

proof

assume A1: f is double-one-to-one ; :: thesis: ( ( for x being object holds f . x is one-to-one ) & ( for x, y being object st x <> y holds
rng (f . x) misses rng (f . y) ) )
hence for x being object holds f . x is one-to-one ; :: thesis: for x, y being object st x <> y holds
rng (f . x) misses rng (f . y)
let x, y be object ; :: thesis: ( x <> y implies rng (f . x) misses rng (f . y) )
assume A2: x <> y ; :: thesis: rng (f . x) misses rng (f . y)
assume rng (f . x) meets rng (f . y) ; :: thesis: contradiction
then consider z being object such that
A3: ( z in rng (f . x) & z in rng (f . y) ) by XBOOLE_0:3;
consider w1 being object such that
A4: ( w1 in dom (f . x) & (f . x) . w1 = z ) by A3, FUNCT_1:def 3;
consider w2 being object such that
A5: ( w2 in dom (f . y) & (f . y) . w2 = z ) by A3, FUNCT_1:def 3;
A6: f _ (x,w1) = f _ (y,w2) by A4, A5;
A7: x in dom f

proof

assume not x in dom f ; :: thesis: contradiction
then f . x = {} by FUNCT_1:def 2;
hence contradiction by A4; :: thesis: verum

end;

y in dom f

proof

assume not y in dom f ; :: thesis: contradiction
then f . y = {} by FUNCT_1:def 2;
hence contradiction by A5; :: thesis: verum

end;

hence contradiction by A4, A5, A1, A6, A7, A2; :: thesis: verum

end;

assume that
A8: for x being object holds f . x is one-to-one and
A9: for x, y being object st x <> y holds
rng (f . x) misses rng (f . y) ; :: thesis: f is double-one-to-one
let x1, x2, y1, y2 be object ; :: according to FLEXARY1:def 6 :: thesis: ( x1 in dom f & y1 in dom (f . x1) & x2 in dom f & y2 in dom (f . x2) & f _ (x1,y1) = f _ (x2,y2) implies ( x1 = x2 & y1 = y2 ) )
assume A10: ( x1 in dom f & y1 in dom (f . x1) & x2 in dom f & y2 in dom (f . x2) & f _ (x1,y1) = f _ (x2,y2) ) ; :: thesis: ( x1 = x2 & y1 = y2 )
A11: (f . x1) . y1 in rng (f . x1) by A10, FUNCT_1:def 3;
(f . x2) . y2 in rng (f . x2) by A10, FUNCT_1:def 3;
then ( x1 = x2 & (f . x1) . y1 = (f . x2) . y2 & f . x1 is one-to-one ) by A11, A10, XBOOLE_0:3, A8, A9;
hence ( x1 = x2 & y1 = y2 ) by A10; :: thesis: verum