let n be Element of NAT ; :: thesis: for X, Y being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds (X + p) (O) Y = (X (O) Y) + p
let X, Y be Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) holds (X + p) (O) Y = (X (O) Y) + p
let p be Point of (TOP-REAL n); :: thesis: (X + p) (O) Y = (X (O) Y) + p
thus (X + p) (O) Y = ((X (-) Y) + p) (+) Y by Th14
.= (X (O) Y) + p by Th15 ; :: thesis: verum