let N be Matrix of 3,REAL; :: thesis: for uf being FinSequence of REAL st uf = 0. (TOP-REAL 3) holds
N * uf = 0. (TOP-REAL 3)
let uf be FinSequence of REAL ; :: thesis: ( uf = 0. (TOP-REAL 3) implies N * uf = 0. (TOP-REAL 3) )
assume A1: uf = 0. (TOP-REAL 3) ; :: thesis: N * uf = 0. (TOP-REAL 3)
reconsider M = N as Matrix of 3,F_Real ;
consider n1, n2, n3, n4, n5, n6, n7, n8, n9 being Element of F_Real such that
A2: M = <*<*n1,n2,n3*>,<*n4,n5,n6*>,<*n7,n8,n9*>*> by PASCAL:3;
reconsider r1 = n1, r2 = n2, r3 = n3, r4 = n4, r5 = n5, r6 = n6, r7 = n7, r8 = n8, r9 = n9 as Element of REAL ;
reconsider z = 0. (TOP-REAL 3) as Element of (TOP-REAL 3) ;
reconsider p = <*0,0,0*> as FinSequence of REAL by EUCLID:24, EUCLID_5:4;
reconsider z1 = z `1 , z2 = z `2 , z3 = z `3 as Element of REAL by XREAL_0:def 1;
( z = <*0,0,0*> & z = <*z1,z2,z3*> ) by EUCLID_5:3, EUCLID_5:4;
then A3: ( z1 = 0 & z2 = 0 & z3 = 0 ) by FINSEQ_1:78;
|[(z `1),(z `2),(z `3)]| = p by EUCLID_5:3, EUCLID_5:4;
then N * uf = <*(((r1 * z1) + (r2 * z2)) + (r3 * z3)),(((r4 * z1) + (r5 * z2)) + (r6 * z3)),(((r7 * z1) + (r8 * z2)) + (r9 * z3))*> by A2, A1, EUCLID_5:4, PASCAL:9
.= 0. (TOP-REAL 3) by A3, EUCLID_5:4 ;
hence N * uf = 0. (TOP-REAL 3) ; :: thesis: verum