let u, v be Element of (TOP-REAL 3); :: thesis: for a, b, c, d, e being Real st u = |[a,b,c]| & v = |[d,e,0]| & are_Prop u,v holds
c = 0
let a, b, c, d, e be Real; :: thesis: ( u = |[a,b,c]| & v = |[d,e,0]| & are_Prop u,v implies c = 0 )
assume that
A1: u = |[a,b,c]| and
A2: v = |[d,e,0]| and
A3: are_Prop u,v ; :: thesis: c = 0
consider f being Real such that
f <> 0 and
A5: |[a,b,c]| = f * |[d,e,0]| by A1, A2, A3, ANPROJ_1:1;
f * |[d,e,0]| = |[(f * d),(f * e),(f * 0)]| by EUCLID_5:8;
then c = |[(f * d),(f * e),(f * 0)]| `3 by A5, EUCLID_5:2
.= f * 0 by EUCLID_5:2 ;
hence c = 0 ; :: thesis: verum