set O = OwnSymbolsOf S;
set AT = AllTermsOf S;
deffunc H₁( 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₁(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