defpred S_{1}[ 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_{1}[x,y]

A2: for x being Element of ND (V,A) holds S_{1}[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

A1: for x being Element of ND (V,A) ex y being Element of ND (V,A) st S

proof

consider f being Function of (ND (V,A)),(ND (V,A)) such that
let x be Element of ND (V,A); :: thesis: ex y being Element of ND (V,A) st S_{1}[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_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;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

thus S

A2: for x being Element of ND (V,A) holds S

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