let M be Matrix of 3,F_Real; :: thesis: for a, b, c, d, e, f, g, h, i, x, y, z being Element of F_Real
for v being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & uf = <*x,y,z*> holds
( p = <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> & v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> )
let a, b, c, d, e, f, g, h, i, x, y, z be Element of F_Real; :: thesis: for v being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & uf = <*x,y,z*> holds
( p = <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> & v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> )
let v be Element of (TOP-REAL 3); :: thesis: for uf being FinSequence of F_Real
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & uf = <*x,y,z*> holds
( p = <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> & v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> )
let uf be FinSequence of F_Real; :: thesis: for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & uf = <*x,y,z*> holds
( p = <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> & v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> )
let p be FinSequence of 1 -tuples_on REAL; :: thesis: ( p = M * uf & v = M2F p & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & uf = <*x,y,z*> implies ( p = <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> & v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> ) )
assume A1: ( p = M * uf & v = M2F p & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & uf = <*x,y,z*> ) ; :: thesis: ( p = <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> & v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> )
then A2: len uf = 3 by FINSEQ_1:45;
A3: len <*uf*> = 1 by FINSEQ_1:39;
rng <*uf*> = {uf} by FINSEQ_1:39;
then uf in rng <*uf*> by TARSKI:def 1;
then A4: width <*uf*> = 3 by A2, A3, MATRIX_0:def 3;
then A5: width (<*uf*> @) = len <*uf*> by MATRIX_0:29
.= 1 by FINSEQ_1:39 ;
len (<*uf*> @) = 3 by MATRIX_0:def 6, A4;
then A6: <*uf*> @ is Matrix of 3,1,F_Real by A5, MATRIX_0:20;
( uf . 1 = x & uf . 2 = y & uf . 3 = z ) by A1, FINSEQ_1:45;
then A8: <*uf*> @ = <*<*x*>,<*y*>,<*z*>*> by A2, ANPROJ_8:77;
thus A9: p = M * (<*uf*> @) by A1, LAPLACE:def 9
.= <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> by A1, A8, A6, ANPROJ_9:7 ; :: thesis: v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*>
now :: thesis: ( len p = 3 & (p . 1) . 1 = ((a * x) + (b * y)) + (c * z) & (p . 2) . 1 = ((d * x) + (e * y)) + (f * z) & (p . 3) . 1 = ((g * x) + (h * y)) + (i * z) )
thus len p = 3 by A9, FINSEQ_1:45; :: thesis: ( (p . 1) . 1 = ((a * x) + (b * y)) + (c * z) & (p . 2) . 1 = ((d * x) + (e * y)) + (f * z) & (p . 3) . 1 = ((g * x) + (h * y)) + (i * z) )
p . 1 = <*(((a * x) + (b * y)) + (c * z))*> by A9, FINSEQ_1:45;
hence (p . 1) . 1 = ((a * x) + (b * y)) + (c * z) by FINSEQ_1:40; :: thesis: ( (p . 2) . 1 = ((d * x) + (e * y)) + (f * z) & (p . 3) . 1 = ((g * x) + (h * y)) + (i * z) )
p . 2 = <*(((d * x) + (e * y)) + (f * z))*> by A9, FINSEQ_1:45;
hence (p . 2) . 1 = ((d * x) + (e * y)) + (f * z) by FINSEQ_1:40; :: thesis: (p . 3) . 1 = ((g * x) + (h * y)) + (i * z)
p . 3 = <*(((g * x) + (h * y)) + (i * z))*> by A9, FINSEQ_1:45;
hence (p . 3) . 1 = ((g * x) + (h * y)) + (i * z) by FINSEQ_1:40; :: thesis: verum
end;
hence v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> by A1, ANPROJ_8:def 2; :: thesis: verum