let F be functional compatible set ; :: thesis: ( ( for f1 being Function st f1 in F holds
( f1 is one-to-one & ( for f2 being Function st f2 in F & f1 <> f2 holds
rng f1 misses rng f2 ) ) ) implies union F is one-to-one )
assume A1: for f1 being Function st f1 in F holds
( f1 is one-to-one & ( for f2 being Function st f2 in F & f1 <> f2 holds
rng f1 misses rng f2 ) ) ; :: thesis: union F is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom (union F) & x2 in dom (union F) & (union F) . x1 = (union F) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (union F) & x2 in dom (union F) & (union F) . x1 = (union F) . x2 implies x1 = x2 )
assume A2: ( x1 in dom (union F) & x2 in dom (union F) & (union F) . x1 = (union F) . x2 ) ; :: thesis: x1 = x2
then [x1,((union F) . x1)] in union F by FUNCT_1:1;
then consider X1 being set such that
A3: ( [x1,((union F) . x1)] in X1 & X1 in F ) by TARSKI:def 4;
reconsider f1 = X1 as Function by A3;
A4: ( x1 in dom f1 & f1 . x1 = (union F) . x1 ) by A3, FUNCT_1:1;
[x2,((union F) . x2)] in union F by A2, FUNCT_1:1;
then consider X2 being set such that
A5: ( [x2,((union F) . x2)] in X2 & X2 in F ) by TARSKI:def 4;
reconsider f2 = X2 as Function by A5;
A6: ( x2 in dom f2 & f2 . x2 = (union F) . x2 ) by A5, FUNCT_1:1;
then A7: f1 . x1 = f2 . x2 by A2, A4;
( f1 . x1 in rng f1 & f2 . x2 in rng f2 ) by A4, A6, FUNCT_1:3;
then f1 = f2 by A1, A3, A5, A7, XBOOLE_0:3;
hence x1 = x2 by A1, A3, A4, A6, A7, FUNCT_1:def 4; :: thesis: verum

end;

hence union F is one-to-one by FUNCT_1:def 4; :: thesis: verum