let n be Nat; :: thesis: {(0* n)} is linear_manifold
let x, y be Element of REAL n; :: according to EUCLID_7:def 8 :: thesis: for a, b being Element of REAL st x in {(0* n)} & y in {(0* n)} holds
(a * x) + (b * y) in {(0* n)}
let a, b be Element of REAL ; :: thesis: ( x in {(0* n)} & y in {(0* n)} implies (a * x) + (b * y) in {(0* n)} )
assume that
A1: x in {(0* n)} and
A2: y in {(0* n)} ; :: thesis: (a * x) + (b * y) in {(0* n)}
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A3: y = 0* n by A2, TARSKI:def 1;
x = 0* n by A1, TARSKI:def 1;
then (a * x) + (b * y) = (0* nn) + (b * (0* nn)) by A3, EUCLID_4:2
.= (0* nn) + (0* nn) by EUCLID_4:2
.= 0* nn by EUCLID_4:1 ;
hence (a * x) + (b * y) in {(0* n)} by TARSKI:def 1; :: thesis: verum