let P be mutually-disjoint set ; :: thesis: for x being Subset of ()
for f being Function of x,P st ( for a being object st a in x holds
a in f . a ) holds
( x is independent iff f is one-to-one )

let x be Subset of (); :: thesis: for f being Function of x,P st ( for a being object st a in x holds
a in f . a ) holds
( x is independent iff f is one-to-one )

let f be Function of x,P; :: thesis: ( ( for a being object st a in x holds
a in f . a ) implies ( x is independent iff f is one-to-one ) )

assume A1: for a being object st a in x holds
a in f . a ; :: thesis: ( x is independent iff f is one-to-one )
hereby :: thesis: ( f is one-to-one implies x is independent )
assume A2: x is independent ; :: thesis: f is one-to-one
thus f is one-to-one :: thesis: verum
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in K49(f) or not b in K49(f) or not f . a = f . b or a = b )
assume that
A3: a in dom f and
A4: b in dom f ; :: thesis: ( not f . a = f . b or a = b )
A5: f . b in rng f by ;
f . a in rng f by ;
then reconsider D1 = f . a, D2 = f . b as Element of P by A5;
a in D1 by A1, A3;
then A6: a in x /\ D1 by ;
consider d2 being Element of D2 such that
A7: x /\ D2 c= {d2} by ;
b in D2 by A1, A4;
then b in x /\ D2 by ;
then b = d2 by ;
hence ( not f . a = f . b or a = b ) by ; :: thesis: verum
end;
end;
assume A8: f is one-to-one ; :: thesis: x is independent
now :: thesis: for D being Element of P holds
not for d being Element of D holds x /\ D c/= {d}
let D be Element of P; :: thesis: not for d being Element of D holds x /\ D c/= {d}
set d1 = the Element of D;
assume A9: for d being Element of D holds x /\ D c/= {d} ; :: thesis: contradiction
then x /\ D c/= { the Element of D} ;
then consider d2 being object such that
A10: d2 in x /\ D and
d2 nin { the Element of D} ;
A11: d2 in D by ;
A12: d2 in x by ;
then d2 in f . d2 by A1;
then A13: f . d2 meets D by ;
the carrier of () = union P by Def7;
then ex y being set st
( d2 in y & y in P ) by ;
then A14: dom f = x by FUNCT_2:def 1;
then f . d2 in rng f by ;
then A15: f . d2 = D by ;
x /\ D c= {d2}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x /\ D or a in {d2} )
assume A16: a in x /\ D ; :: thesis: a in {d2}
then A17: a in x by XBOOLE_0:def 4;
A18: a in D by ;
a in f . a by ;
then A19: f . a meets D by ;
f . a in rng f by ;
then f . a = D by ;
then a = d2 by A8, A12, A14, A15, A17;
hence a in {d2} by TARSKI:def 1; :: thesis: verum
end;
hence contradiction by A9, A11; :: thesis: verum
end;
hence x is independent by Th8; :: thesis: verum