defpred S₁[ set , set ] means for x' being Function st $1 = x' holds
$2 = x' . x;

A5: now

let q be set ; :: thesis: ( q in product f implies ex y being set st S₁[q,y] )
assume q in product f ; :: thesis: ex y being set st S₁[q,y]
then reconsider q1 = q as Function ;
take y = q1 . x; :: thesis: S₁[q,y]
thus S₁[q,y] ; :: thesis: verum

end;

consider F being Function such that
A6: ( dom F = product f & ( for a being set st a in product f holds
S₁[a,F . a] ) ) from CLASSES1:sch 1(A5);
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 A6; :: thesis: verum