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;

now :: thesis: not x in A

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;

hence x in B \ A by A13, XBOOLE_0:def 5; :: thesis: A \/ {x} in the_family_of (ProdMatroid P)
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}

let D be set ; :: thesis: ( D in P implies ex x9 being set st Ax /\ x9 c= {b₂} )
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 ) ;

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

reconsider x9 = x9 as set by TARSKI:1;
take x9 = x9; :: thesis: Ax /\ D c= {x9}
A /\ D c= {}

proof

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;

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

end;

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

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;

end;

end;

hence A \/ {x} in the_family_of (ProdMatroid P) by A1; :: thesis: verum