set O = OwnSymbolsOf S;

set AT = AllTermsOf S;

deffunc H_{1}( Element of OwnSymbolsOf S) -> set = (I . $1) quotient E;

consider f being Function such that

A1: ( dom f = OwnSymbolsOf S & ( for d being Element of OwnSymbolsOf S holds f . d = H_{1}(d) ) )
from FUNCT_1:sch 4();

take f ; :: thesis: ( dom f = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds f . o = (I . o) quotient E ) )

thus ( dom f = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds f . o = (I . o) quotient E ) ) by A1; :: thesis: verum

set AT = AllTermsOf S;

deffunc H

consider f being Function such that

A1: ( dom f = OwnSymbolsOf S & ( for d being Element of OwnSymbolsOf S holds f . d = H

take f ; :: thesis: ( dom f = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds f . o = (I . o) quotient E ) )

thus ( dom f = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds f . o = (I . o) quotient E ) ) by A1; :: thesis: verum