set Sm = the Symbols of s \/ the Symbols of t;
set X = [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t):];
let f, g be 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}:]; :: thesis: ( ( for x being Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t):] holds f . x = Uniontran s,t,x ) & ( for x being Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t):] holds g . x = Uniontran s,t,x ) implies f = g )
assume that
A2: for x being Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t):] holds f . x = Uniontran s,t,x and
A3: for x being Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t):] holds g . x = Uniontran s,t,x ; :: thesis: f = g

now

let x be Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t):]; :: thesis: f . x = g . x
thus f . x = Uniontran s,t,x by A2
.= g . x by A3 ; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum