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₁( 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₁(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