let U1, U2 be Function of (UPS (S2,T1)),(UPS (S1,T2)); :: thesis: ( ( for h being directed-sups-preserving Function of S2,T1 holds U1 . h = (g * h) * f ) & ( for h being directed-sups-preserving Function of S2,T1 holds U2 . h = (g * h) * f ) implies U1 = U2 )
assume that
A5: for h being directed-sups-preserving Function of S2,T1 holds U1 . h = (g * h) * f and
A6: for h being directed-sups-preserving Function of S2,T1 holds U2 . h = (g * h) * f ; :: thesis: U1 = U2
for x being object st x in the carrier of (UPS (S2,T1)) holds
U1 . x = U2 . x
proof
let x be object ; :: thesis: ( x in the carrier of (UPS (S2,T1)) implies U1 . x = U2 . x )
assume x in the carrier of (UPS (S2,T1)) ; :: thesis: U1 . x = U2 . x
then reconsider h = x as directed-sups-preserving Function of S2,T1 by Def4;
thus U1 . x = (g * h) * f by A5
.= U2 . x by A6 ; :: thesis: verum
end;
hence U1 = U2 by FUNCT_2:12; :: thesis: verum