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, B be finite Subset of (ProdMatroid P); :: according to MATROID0:def 4 :: thesis: ( A in the_family_of (ProdMatroid P) & B in the_family_of (ProdMatroid P) & card B = (card A) + 1 implies ex e being Element of (ProdMatroid P) st

( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) )

assume that

A2: A in the_family_of (ProdMatroid P) and

A3: B in the_family_of (ProdMatroid P) ; :: thesis: ( not card B = (card A) + 1 or ex e being Element of (ProdMatroid P) st

( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) )

consider f being Function of A,P such that

A4: for a being object st a in A holds

a in f . a by Th9;

assume card B = (card A) + 1 ; :: thesis: ex e being Element of (ProdMatroid P) st

( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) )

then A5: card B > card A by NAT_1:13;

consider g being Function of B,P such that

A6: for a being object st a in B holds

a in g . a by Th9;

A7: the carrier of (ProdMatroid P) = union P by Def7;

then ( P = {} implies A = {} ) by ZFMISC_1:2;

then A8: dom f = A by FUNCT_2:def 1;

reconsider A9 = rng f, B9 = rng g as finite set ;

A9: A is independent by A2;

then f is one-to-one by A4, Th10;

then A,A9 are_equipotent by A8, WELLORD2:def 4;

then A10: card A = card A9 by CARD_1:5;

( P = {} implies B = {} ) by A7, ZFMISC_1:2;

then A11: dom g = B by FUNCT_2:def 1;

B is independent by A3;

then g is one-to-one by A6, Th10;

then B,B9 are_equipotent by A11, WELLORD2:def 4;

then card B = card B9 by CARD_1:5;

then consider a being set such that

A12: a in B9 \ A9 by A10, A5, Th5;

consider x9 being object such that

A13: x9 in B and

A14: a = g . x9 by A11, A12, FUNCT_1:def 3;

reconsider x = x9 as Element of (ProdMatroid P) by A13;

take x ; :: thesis: ( x in B \ A & A \/ {x} in the_family_of (ProdMatroid P) )

A15: a nin A9 by A12, XBOOLE_0:def 5;

reconsider xx = {x} as Subset of (ProdMatroid P) by A13, ZFMISC_1:31;

reconsider Ax = A \/ xx as Subset of (union P) by Def7;

A20: a in B9 by A12;

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, B be finite Subset of (ProdMatroid P); :: according to MATROID0:def 4 :: thesis: ( A in the_family_of (ProdMatroid P) & B in the_family_of (ProdMatroid P) & card B = (card A) + 1 implies ex e being Element of (ProdMatroid P) st

( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) )

assume that

A2: A in the_family_of (ProdMatroid P) and

A3: B in the_family_of (ProdMatroid P) ; :: thesis: ( not card B = (card A) + 1 or ex e being Element of (ProdMatroid P) st

( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) )

consider f being Function of A,P such that

A4: for a being object st a in A holds

a in f . a by Th9;

assume card B = (card A) + 1 ; :: thesis: ex e being Element of (ProdMatroid P) st

( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) )

then A5: card B > card A by NAT_1:13;

consider g being Function of B,P such that

A6: for a being object st a in B holds

a in g . a by Th9;

A7: the carrier of (ProdMatroid P) = union P by Def7;

then ( P = {} implies A = {} ) by ZFMISC_1:2;

then A8: dom f = A by FUNCT_2:def 1;

reconsider A9 = rng f, B9 = rng g as finite set ;

A9: A is independent by A2;

then f is one-to-one by A4, Th10;

then A,A9 are_equipotent by A8, WELLORD2:def 4;

then A10: card A = card A9 by CARD_1:5;

( P = {} implies B = {} ) by A7, ZFMISC_1:2;

then A11: dom g = B by FUNCT_2:def 1;

B is independent by A3;

then g is one-to-one by A6, Th10;

then B,B9 are_equipotent by A11, WELLORD2:def 4;

then card B = card B9 by CARD_1:5;

then consider a being set such that

A12: a in B9 \ A9 by A10, A5, Th5;

consider x9 being object such that

A13: x9 in B and

A14: a = g . x9 by A11, A12, FUNCT_1:def 3;

reconsider x = x9 as Element of (ProdMatroid P) by A13;

take x ; :: thesis: ( x in B \ A & A \/ {x} in the_family_of (ProdMatroid P) )

A15: a nin A9 by A12, XBOOLE_0:def 5;

now :: thesis: not x in A

hence
x in B \ A
by A13, XBOOLE_0:def 5; :: thesis: A \/ {x} in the_family_of (ProdMatroid P)A16:
x in g . x
by A6, A13;

assume A17: x in A ; :: thesis: contradiction

then x in f . x by A4;

then A18: f . x meets g . x by A16, XBOOLE_0:3;

A19: g . x in rng g by A11, A13, FUNCT_1:def 3;

f . x in rng f by A8, A17, FUNCT_1:def 3;

hence contradiction by A15, A14, A19, A18, TAXONOM2:def 5; :: thesis: verum

end;assume A17: x in A ; :: thesis: contradiction

then x in f . x by A4;

then A18: f . x meets g . x by A16, XBOOLE_0:3;

A19: g . x in rng g by A11, A13, FUNCT_1:def 3;

f . x in rng f by A8, A17, FUNCT_1:def 3;

hence contradiction by A15, A14, A19, A18, TAXONOM2:def 5; :: thesis: verum

reconsider xx = {x} as Subset of (ProdMatroid P) by A13, ZFMISC_1:31;

reconsider Ax = A \/ xx as Subset of (union P) by Def7;

A20: a in B9 by A12;

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

ex x9 being set st Ax /\ D c= {x9}

hence
A \/ {x} in the_family_of (ProdMatroid P)
by A1; :: thesis: verumex x9 being set st Ax /\ D c= {x9}

let D be set ; :: thesis: ( D in P implies ex x9 being set st Ax /\ x9 c= {b_{2}} )

A21: Ax /\ D = (A /\ D) \/ (xx /\ D) by XBOOLE_1:23;

assume A22: D in P ; :: thesis: ex x9 being set st Ax /\ x9 c= {b_{2}}

then consider d being Element of D such that

A23: A /\ D c= {d} by A9, Th8;

end;A21: Ax /\ D = (A /\ D) \/ (xx /\ D) by XBOOLE_1:23;

assume A22: D in P ; :: thesis: ex x9 being set st Ax /\ x9 c= {b

then consider d being Element of D such that

A23: A /\ D c= {d} by A9, Th8;

per cases
( D = a or D <> a )
;

end;

suppose A24:
D = a
; :: thesis: ex x9 being set st Ax /\ x9 c= {b_{2}}

reconsider x9 = x9 as set by TARSKI:1;

take x9 = x9; :: thesis: Ax /\ D c= {x9}

A /\ D c= {}

hence Ax /\ D c= {x9} by A21, XBOOLE_1:17; :: thesis: verum

end;take x9 = x9; :: thesis: Ax /\ D c= {x9}

A /\ D c= {}

proof

then
A /\ D = {}
;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in A /\ D or z in {} )

assume A25: z in A /\ D ; :: thesis: z in {}

then A26: z in D by XBOOLE_0:def 4;

A27: z in A by A25, XBOOLE_0:def 4;

then z in f . z by A4;

then A28: D meets f . z by A26, XBOOLE_0:3;

f . z in rng f by A8, A27, FUNCT_1:def 3;

hence z in {} by A20, A15, A24, A28, TAXONOM2:def 5; :: thesis: verum

end;assume A25: z in A /\ D ; :: thesis: z in {}

then A26: z in D by XBOOLE_0:def 4;

A27: z in A by A25, XBOOLE_0:def 4;

then z in f . z by A4;

then A28: D meets f . z by A26, XBOOLE_0:3;

f . z in rng f by A8, A27, FUNCT_1:def 3;

hence z in {} by A20, A15, A24, A28, TAXONOM2:def 5; :: thesis: verum

hence Ax /\ D c= {x9} by A21, XBOOLE_1:17; :: thesis: verum

suppose A29:
D <> a
; :: thesis: ex d being set st Ax /\ d c= {b_{2}}

a in rng g
by A11, A13, A14, FUNCT_1:def 3;

then A30: a misses D by A22, A29, TAXONOM2:def 5;

x in a by A6, A13, A14;

then x nin D by A30, XBOOLE_0:3;

then xx c/= D by ZFMISC_1:31;

then A31: xx /\ D <> xx by XBOOLE_1:17;

reconsider d = d as set ;

take d = d; :: thesis: Ax /\ D c= {d}

xx /\ D c= xx by XBOOLE_1:17;

then xx /\ D = {} by A31, ZFMISC_1:33;

hence Ax /\ D c= {d} by A23, A21; :: thesis: verum

end;then A30: a misses D by A22, A29, TAXONOM2:def 5;

x in a by A6, A13, A14;

then x nin D by A30, XBOOLE_0:3;

then xx c/= D by ZFMISC_1:31;

then A31: xx /\ D <> xx by XBOOLE_1:17;

reconsider d = d as set ;

take d = d; :: thesis: Ax /\ D c= {d}

xx /\ D c= xx by XBOOLE_1:17;

then xx /\ D = {} by A31, ZFMISC_1:33;

hence Ax /\ D c= {d} by A23, A21; :: thesis: verum