let P be set ; :: thesis: for A being Subset of (ProdMatroid P) holds
( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} )
set M = ProdMatroid P;
A1: the_family_of (ProdMatroid P) = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} } by Def7;
let A be Subset of (ProdMatroid P); :: thesis: ( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} )
A2: the carrier of (ProdMatroid P) = union P by Def7;
thus ( A is independent implies for D being Element of P ex d being Element of D st A /\ D c= {d} ) :: thesis: ( ( for D being Element of P ex d being Element of D st A /\ D c= {d} ) implies A is independent )
proof
assume A in the_family_of (ProdMatroid P) ; :: according to MATROID0:def 2 :: thesis: for D being Element of P ex d being Element of D st A /\ D c= {d}
then A3: ex B being Subset of (union P) st
( A = B & ( for D being set st D in P holds
ex d being set st B /\ D c= {d} ) ) by A1;
let D be Element of P; :: thesis: ex d being Element of D st A /\ D c= {d}
( P = {} implies ( A = {} & {} /\ D = {} ) ) by A2, ZFMISC_1:2;
then ( P = {} implies A /\ D c= {1} ) ;
then consider d being set such that
A4: A /\ D c= {d} by A3;
set d0 = the Element of D;
now :: thesis: ( d nin D implies A /\ D c= { the Element of D} )
assume d nin D ; :: thesis: A /\ D c= { the Element of D}
then d nin A /\ D by XBOOLE_0:def 4;
then A /\ D <> {d} by TARSKI:def 1;
then A /\ D = {} by A4, ZFMISC_1:33;
hence A /\ D c= { the Element of D} ; :: thesis: verum
end;
hence ex d being Element of D st A /\ D c= {d} by A4; :: thesis: verum
end;
assume A5: for D being Element of P ex d being Element of D st A /\ D c= {d} ; :: thesis: A is independent
A6: now :: thesis: for D being set st D in P holds
ex d being set st A /\ D c= {d}
let D be set ; :: thesis: ( D in P implies ex d being set st A /\ D c= {d} )
assume D in P ; :: thesis: ex d being set st A /\ D c= {d}
then ex d being Element of D st A /\ D c= {d} by A5;
hence ex d being set st A /\ D c= {d} ; :: thesis: verum
end;
the carrier of (ProdMatroid P) = union P by Def7;
hence A in the_family_of (ProdMatroid P) by A1, A6; :: according to MATROID0:def 2 :: thesis: verum