defpred S₁[ 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

A1: now :: thesis: for a being object st a in x holds
ex y being object st
( y in P & S₁[a,y] )

let a be object ; :: thesis: ( a in x implies ex y being object st
( y in P & S₁[a,y] ) )
assume a in x ; :: thesis: ex y being object st
( y in P & S₁[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₁[a,y] ) ; :: thesis: verum

end;

consider f being Function of x,P such that
A2: for a being object st a in x holds
S₁[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₁[a,f . a] by A2;
hence a in f . a ; :: thesis: verum