set SS = AllSymbolsOf S;

deffunc H_{1}( Element of (((AllSymbolsOf S) *) \ {{}}) * ) -> string of S = s -compound $1;

consider f being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) such that

A1: for x being Element of (((AllSymbolsOf S) *) \ {{}}) * holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

take f ; :: thesis: for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds f . V = s -compound V

thus for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds f . V = s -compound V by A1; :: thesis: verum

deffunc H

consider f being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) such that

A1: for x being Element of (((AllSymbolsOf S) *) \ {{}}) * holds f . x = H

take f ; :: thesis: for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds f . V = s -compound V

thus for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds f . V = s -compound V by A1; :: thesis: verum