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 )

hence A in the_family_of (ProdMatroid P) by A1, A6; :: according to MATROID0:def 2 :: thesis: verum

( 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 A5:
for D being Element of P ex d being Element of D st A /\ D c= {d}
; :: thesis: A is independent
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;

end;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} )

hence
ex d being Element of D st A /\ D c= {d}
by A4; :: thesis: verumassume
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;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

A6: now :: thesis: for D being set st D in P holds

ex d being set st A /\ D c= {d}

the carrier of (ProdMatroid P) = union P
by Def7;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;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

hence A in the_family_of (ProdMatroid P) by A1, A6; :: according to MATROID0:def 2 :: thesis: verum