defpred S₁[ set , set ] means $1 in $2;
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 set 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 set st a in x holds
a in f . a

A1: now

let a be set ; :: thesis: ( a in x implies ex y being set st
( y in P & S₁[a,y] ) )
assume a in x ; :: thesis: ex y being set st
( y in P & S₁[a,y] )
then a in the carrier of (ProdMatroid P) ;
then a in union P by Def8;
then ex y being set st
( a in y & y in P ) by TARSKI:def 4;
hence ex y being set st
( y in P & S₁[a,y] ) ; :: thesis: verum

end;

consider f being Function of x,P such that
A2: for a being set st a in x holds
S₁[a,f . a] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for a being set st a in x holds
a in f . a
thus for a being set st a in x holds
a in f . a by A2; :: thesis: verum