defpred S_{1}[ object , object ] means ex D2 being set st

( D2 = $2 & $1 in D2 );

let P be mutually-disjoint set ; :: thesis: for x being Subset of (ProdMatroid P) ex f being Function of x,P st

for a being object st a in x holds

a in f . a

let x be Subset of (ProdMatroid P); :: thesis: ex f being Function of x,P st

for a being object st a in x holds

a in f . a

A2: for a being object st a in x holds

S_{1}[a,f . a]
from FUNCT_2:sch 1(A1);

take f ; :: thesis: for a being object st a in x holds

a in f . a

let a be object ; :: thesis: ( a in x implies a in f . a )

assume a in x ; :: thesis: a in f . a

then S_{1}[a,f . a]
by A2;

hence a in f . a ; :: thesis: verum

( D2 = $2 & $1 in D2 );

let P be mutually-disjoint set ; :: thesis: for x being Subset of (ProdMatroid P) ex f being Function of x,P st

for a being object st a in x holds

a in f . a

let x be Subset of (ProdMatroid P); :: thesis: ex f being Function of x,P st

for a being object st a in x holds

a in f . a

A1: now :: thesis: for a being object st a in x holds

ex y being object st

( y in P & S_{1}[a,y] )

consider f being Function of x,P such that ex y being object st

( y in P & S

let a be object ; :: thesis: ( a in x implies ex y being object st

( y in P & S_{1}[a,y] ) )

assume a in x ; :: thesis: ex y being object st

( y in P & S_{1}[a,y] )

then a in the carrier of (ProdMatroid P) ;

then a in union P by Def7;

then ex y being set st

( a in y & y in P ) by TARSKI:def 4;

hence ex y being object st

( y in P & S_{1}[a,y] )
; :: thesis: verum

end;( y in P & S

assume a in x ; :: thesis: ex y being object st

( y in P & S

then a in the carrier of (ProdMatroid P) ;

then a in union P by Def7;

then ex y being set st

( a in y & y in P ) by TARSKI:def 4;

hence ex y being object st

( y in P & S

A2: for a being object st a in x holds

S

take f ; :: thesis: for a being object st a in x holds

a in f . a

let a be object ; :: thesis: ( a in x implies a in f . a )

assume a in x ; :: thesis: a in f . a

then S

hence a in f . a ; :: thesis: verum