let P be mutually-disjoint set ; :: thesis: for x being Subset of (ProdMatroid P)
for f being Function of x,P st ( for a being set st a in x holds
a in f . a ) holds
( x is independent iff f is one-to-one )
let x be Subset of (ProdMatroid P); :: thesis: for f being Function of x,P st ( for a being set 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 set st a in x holds
a in f . a ) implies ( x is independent iff f is one-to-one ) )
assume 01: for a being set 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 03: x is independent ; :: thesis: f is one-to-one
thus f is one-to-one :: thesis: verum

proof

let a, b be set ; :: according to FUNCT_1:def 8 :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume ( a in dom f & b in dom f ) ; :: thesis: ( not f . a = f . b or a = b )
then 06: ( f . a in rng f & f . b in rng f & a in x & b in x ) by FUNCT_1:def 5;
then reconsider D1 = f . a, D2 = f . b as Element of P ;
consider d1 being Element of D1 such that
04: x /\ D1 c= {d1} by 03, Th10;
consider d2 being Element of D2 such that
05: x /\ D2 c= {d2} by 03, Th10;
( a in D1 & b in D2 ) by 01, 06;
then 07: ( a in x /\ D1 & b in x /\ D2 ) by 06, XBOOLE_0:def 4;
then ( a = d1 & b = d2 ) by 04, 05, TARSKI:def 1;
hence ( not f . a = f . b or a = b ) by 05, 07, TARSKI:def 1; :: thesis: verum

end;

end;

assume 08: f is one-to-one ; :: thesis: x is independent

now

let D be Element of P; :: thesis: not for d being Element of D holds x /\ D c/= {d}
assume 09: for d being Element of D holds x /\ D c/= {d} ; :: thesis: contradiction
consider d1 being Element of D;
x /\ D c/= {d1} by 09;
then consider d2 being set such that
010: ( d2 in x /\ D & d2 nin {d1} ) by TARSKI:def 3;
011: ( d2 in x & d2 in D & d1 <> d2 ) by 010, XBOOLE_0:def 4, TARSKI:def 1;
the carrier of (ProdMatroid P) = union P by Def4;
then ex y being set st
( d2 in y & y in P ) by 011, TARSKI:def 4;
then 012: ( dom f = x & D in P ) by FUNCT_2:def 1;
then ( d2 in f . d2 & f . d2 in rng f ) by 01, 011, FUNCT_1:def 5;
then ( f . d2 meets D & f . d2 in P ) by 011, XBOOLE_0:3;
then 013: f . d2 = D by TAXONOM2:def 5;
x /\ D c= {d2}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in x /\ D or a in {d2} )
assume a in x /\ D ; :: thesis: a in {d2}
then 014: ( a in x & a in D ) by XBOOLE_0:def 4;
then ( a in f . a & f . a in rng f ) by 01, 012, FUNCT_1:def 5;
then ( f . a meets D & f . a in P ) by 014, XBOOLE_0:3;
then f . a = D by TAXONOM2:def 5;
then a = d2 by 011, 012, 013, 014, 08, FUNCT_1:def 8;
hence a in {d2} by TARSKI:def 1; :: thesis: verum

end;

hence contradiction by 09, 011; :: thesis: verum

end;

hence x is independent by Th10; :: thesis: verum