let t be Real; :: thesis: for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)
let n be Element of NAT ; :: thesis: for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)
let X, Y be Subset of (TOP-REAL n); :: thesis: ( t <> 0 implies t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) )
assume t <> 0 ; :: thesis: t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)
then t (.) (X (o) Y) = (t (.) (X (+) Y)) (-) (t (.) Y) by Th64
.= ((t (.) X) (+) (t (.) Y)) (-) (t (.) Y) by Th63 ;
hence t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) ; :: thesis: verum