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 A1: t <> 0 ; :: thesis: t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y)
t (.) (X (O) Y) = (t (.) (X (-) Y)) (+) (t (.) Y) by Th63
.= ((t (.) X) (-) (t (.) Y)) (+) (t (.) Y) by A1, Th64 ;
hence t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y) ; :: thesis: verum