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 object 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 object 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 object st a in x holds

a in f . a ) implies ( x is independent iff f is one-to-one ) )

assume A1: for a being object st a in x holds

a in f . a ; :: thesis: ( x is independent iff f is one-to-one )

for f being Function of x,P st ( for a being object 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 object 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 object st a in x holds

a in f . a ) implies ( x is independent iff f is one-to-one ) )

assume A1: for a being object 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 A8:
f is one-to-one
; :: thesis: x is independent assume A2:
x is independent
; :: thesis: f is one-to-one

thus f is one-to-one :: thesis: verum

end;thus f is one-to-one :: thesis: verum

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in K49(f) or not b in K49(f) or not f . a = f . b or a = b )

assume that

A3: a in dom f and

A4: b in dom f ; :: thesis: ( not f . a = f . b or a = b )

A5: f . b in rng f by A4, FUNCT_1:def 3;

f . a in rng f by A3, FUNCT_1:def 3;

then reconsider D1 = f . a, D2 = f . b as Element of P by A5;

a in D1 by A1, A3;

then A6: a in x /\ D1 by A3, XBOOLE_0:def 4;

consider d2 being Element of D2 such that

A7: x /\ D2 c= {d2} by A2, Th8;

b in D2 by A1, A4;

then b in x /\ D2 by A4, XBOOLE_0:def 4;

then b = d2 by A7, TARSKI:def 1;

hence ( not f . a = f . b or a = b ) by A7, A6, TARSKI:def 1; :: thesis: verum

end;assume that

A3: a in dom f and

A4: b in dom f ; :: thesis: ( not f . a = f . b or a = b )

A5: f . b in rng f by A4, FUNCT_1:def 3;

f . a in rng f by A3, FUNCT_1:def 3;

then reconsider D1 = f . a, D2 = f . b as Element of P by A5;

a in D1 by A1, A3;

then A6: a in x /\ D1 by A3, XBOOLE_0:def 4;

consider d2 being Element of D2 such that

A7: x /\ D2 c= {d2} by A2, Th8;

b in D2 by A1, A4;

then b in x /\ D2 by A4, XBOOLE_0:def 4;

then b = d2 by A7, TARSKI:def 1;

hence ( not f . a = f . b or a = b ) by A7, A6, TARSKI:def 1; :: thesis: verum

now :: thesis: for D being Element of P holds

not for d being Element of D holds x /\ D c/= {d}

hence
x is independent
by Th8; :: thesis: verumnot for d being Element of D holds x /\ D c/= {d}

let D be Element of P; :: thesis: not for d being Element of D holds x /\ D c/= {d}

set d1 = the Element of D;

assume A9: for d being Element of D holds x /\ D c/= {d} ; :: thesis: contradiction

then x /\ D c/= { the Element of D} ;

then consider d2 being object such that

A10: d2 in x /\ D and

d2 nin { the Element of D} ;

A11: d2 in D by A10, XBOOLE_0:def 4;

A12: d2 in x by A10, XBOOLE_0:def 4;

then d2 in f . d2 by A1;

then A13: f . d2 meets D by A11, XBOOLE_0:3;

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

then ex y being set st

( d2 in y & y in P ) by A10, TARSKI:def 4;

then A14: dom f = x by FUNCT_2:def 1;

then f . d2 in rng f by A12, FUNCT_1:def 3;

then A15: f . d2 = D by A13, TAXONOM2:def 5;

x /\ D c= {d2}

end;set d1 = the Element of D;

assume A9: for d being Element of D holds x /\ D c/= {d} ; :: thesis: contradiction

then x /\ D c/= { the Element of D} ;

then consider d2 being object such that

A10: d2 in x /\ D and

d2 nin { the Element of D} ;

A11: d2 in D by A10, XBOOLE_0:def 4;

A12: d2 in x by A10, XBOOLE_0:def 4;

then d2 in f . d2 by A1;

then A13: f . d2 meets D by A11, XBOOLE_0:3;

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

then ex y being set st

( d2 in y & y in P ) by A10, TARSKI:def 4;

then A14: dom f = x by FUNCT_2:def 1;

then f . d2 in rng f by A12, FUNCT_1:def 3;

then A15: f . d2 = D by A13, TAXONOM2:def 5;

x /\ D c= {d2}

proof

hence
contradiction
by A9, A11; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x /\ D or a in {d2} )

assume A16: a in x /\ D ; :: thesis: a in {d2}

then A17: a in x by XBOOLE_0:def 4;

A18: a in D by A16, XBOOLE_0:def 4;

a in f . a by A1, A17;

then A19: f . a meets D by A18, XBOOLE_0:3;

f . a in rng f by A14, A17, FUNCT_1:def 3;

then f . a = D by A19, TAXONOM2:def 5;

then a = d2 by A8, A12, A14, A15, A17;

hence a in {d2} by TARSKI:def 1; :: thesis: verum

end;assume A16: a in x /\ D ; :: thesis: a in {d2}

then A17: a in x by XBOOLE_0:def 4;

A18: a in D by A16, XBOOLE_0:def 4;

a in f . a by A1, A17;

then A19: f . a meets D by A18, XBOOLE_0:3;

f . a in rng f by A14, A17, FUNCT_1:def 3;

then f . a = D by A19, TAXONOM2:def 5;

then a = d2 by A8, A12, A14, A15, A17;

hence a in {d2} by TARSKI:def 1; :: thesis: verum