take u = |[1,0,0]|; :: according to ANPROJ_2:def 6 :: thesis: ex b₁, b₂ being Element of the carrier of (TOP-REAL 3) st
for b₃, b₄, b₅ being object holds
( not ((b₃ * u) + (b₄ * b₁)) + (b₅ * b₂) = 0. (TOP-REAL 3) or ( b₃ = 0 & b₄ = 0 & b₅ = 0 ) )
take v = |[0,1,0]|; :: thesis: ex b₁ being Element of the carrier of (TOP-REAL 3) st
for b₂, b₃, b₄ being object holds
( not ((b₂ * u) + (b₃ * v)) + (b₄ * b₁) = 0. (TOP-REAL 3) or ( b₂ = 0 & b₃ = 0 & b₄ = 0 ) )
take w = |[0,0,1]|; :: thesis: for b₁, b₂, b₃ being object holds
( not ((b₁ * u) + (b₂ * v)) + (b₃ * w) = 0. (TOP-REAL 3) or ( b₁ = 0 & b₂ = 0 & b₃ = 0 ) )
let a, b, c be Real; :: thesis: ( not ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) or ( a = 0 & b = 0 & c = 0 ) )
assume A1: ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) ; :: thesis: ( a = 0 & b = 0 & c = 0 )
A2: ( |[a,b,c]| `1 = a & |[a,b,c]| `2 = b & |[a,b,c]| `3 = c ) by EUCLID_5:2;
A3: c * w = |[(c * 0),(c * 0),(c * 1)]| by EUCLID_5:8;
( a * u = |[(a * 1),(a * 0),(a * 0)]| & b * v = |[(b * 0),(b * 1),(b * 0)]| ) by EUCLID_5:8;
then ((a * u) + (b * v)) + (c * w) = |[(a + 0),(0 + b),(0 + 0)]| + (c * w) by EUCLID_5:6
.= |[(a + 0),(b + 0),(0 + c)]| by A3, EUCLID_5:6 ;
hence ( a = 0 & b = 0 & c = 0 ) by A1, A2, EUCLID_5:2, EUCLID_5:4; :: thesis: verum