let M be Matrix of 3,F_Real; 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; 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); 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; 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; ( 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*> )
; ( 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
; v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*>
now ( 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) )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; verum