set Sm = the Symbols of s \/ the Symbols of t;

set X = [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):];

deffunc H_{1}( Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):]) -> Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] = Uniontran (s,t,$1);

consider f being Function of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):],[:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] such that

A1: for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

take f ; :: thesis: for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds f . x = Uniontran (s,t,x)

thus for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds f . x = Uniontran (s,t,x) by A1; :: thesis: verum

set X = [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):];

deffunc H

consider f being Function of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):],[:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] such that

A1: for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds f . x = H

take f ; :: thesis: for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds f . x = Uniontran (s,t,x)

thus for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds f . x = Uniontran (s,t,x) by A1; :: thesis: verum