defpred S2[ set , set ] means for g being Function st $1 = g holds
$2 = g . x;
A1: now
let q be set ; :: thesis: ( q in product f implies ex y being set st S2[q,y] )
assume q in product f ; :: thesis: ex y being set st S2[q,y]
then reconsider q1 = q as Function ;
take y = q1 . x; :: thesis: S2[q,y]
thus S2[q,y] ; :: thesis: verum
end;
consider F being Function such that
A2: ( dom F = product f & ( for a being set st a in product f holds
S2[a,F . a] ) ) from CLASSES1:sch 1(A1);
 take F ; :: thesis: ( dom F = product f & ( for y being Function st y in dom F holds
F . y = y . x ) )
thus ( dom F = product f & ( for y being Function st y in dom F holds
F . y = y . x ) ) by A2; :: thesis: verum