defpred S₂[ object , object ] means for g being Function st $1 = g holds
$2 = g . x;

A1: now :: thesis: for q being object st q in product f holds
ex y being object st S₂[q,y]

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

end;

consider F being Function such that
A2: ( dom F = product f & ( for a being object st a in product f holds
S₂[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