let n1, n2, n3 be Element of F_Real; :: thesis: for n, u being Element of (TOP-REAL 3) st n = <*n1,n2,n3*> & u . 3 = 1 holds
|(n,u)| = ((n1 * (u . 1)) + (n2 * (u . 2))) + n3
let n, u be Element of (TOP-REAL 3); :: thesis: ( n = <*n1,n2,n3*> & u . 3 = 1 implies |(n,u)| = ((n1 * (u . 1)) + (n2 * (u . 2))) + n3 )
assume that
A1: n = <*n1,n2,n3*> and
A2: u . 3 = 1 ; :: thesis: |(n,u)| = ((n1 * (u . 1)) + (n2 * (u . 2))) + n3
n = |[(n `1),(n `2),(n `3)]| by EUCLID_5:3;
then A3: ( n `1 = n1 & n `2 = n2 & n `3 = n3 ) by A1, FINSEQ_1:78;
|(n,u)| = ((n1 * (u `1)) + (n2 * (u `2))) + (n3 * (u `3)) by A3, EUCLID_5:29
.= ((n1 * (u . 1)) + (n2 * (u `2))) + (n3 * (u `3)) by EUCLID_5:def 1
.= ((n1 * (u . 1)) + (n2 * (u . 2))) + (n3 * (u `3)) by EUCLID_5:def 2
.= ((n1 * (u . 1)) + (n2 * (u . 2))) + (n3 * (u . 3)) by EUCLID_5:def 3 ;
hence |(n,u)| = ((n1 * (u . 1)) + (n2 * (u . 2))) + n3 by A2; :: thesis: verum