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