defpred S₁[ object , object ] means $2 = naming (V,A,v,$1);
A1: for x being Element of ND (V,A) ex y being Element of ND (V,A) st S₁[x,y]

proof

let x be Element of ND (V,A); :: thesis: ex y being Element of ND (V,A) st S₁[x,y]
set y = naming (V,A,v,x);
naming (V,A,v,x) in ND (V,A) ;
then reconsider y = naming (V,A,v,x) as Element of ND (V,A) ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function of (ND (V,A)),(ND (V,A)) such that
A2: for x being Element of ND (V,A) holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for D being TypeSCNominativeData of V,A holds f . D = naming (V,A,v,D)
let D be TypeSCNominativeData of V,A; :: thesis: f . D = naming (V,A,v,D)
D in ND (V,A) ;
hence f . D = naming (V,A,v,D) by A2; :: thesis: verum