let M be Matrix of 3,F_Real; :: thesis: for MR being Matrix of 3,REAL
for v being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for ufr being FinSequence of REAL
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds
v = MR * ufr
let MR be Matrix of 3,REAL; :: thesis: for v being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for ufr being FinSequence of REAL
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds
v = MR * ufr
let v be Element of (TOP-REAL 3); :: thesis: for uf being FinSequence of F_Real
for ufr being FinSequence of REAL
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds
v = MR * ufr
let uf be FinSequence of F_Real; :: thesis: for ufr being FinSequence of REAL
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds
v = MR * ufr
let ufr be FinSequence of REAL ; :: thesis: for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds
v = MR * ufr
let p be FinSequence of 1 -tuples_on REAL; :: thesis: ( p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M implies v = MR * ufr )
assume that
A1: p = M * uf and
A2: v = M2F p and
A3: len uf = 3 and
A4: uf = ufr and
A5: MR = M ; :: thesis: v = MR * ufr
consider a, b, c, d, e, f, g, h, i being Element of F_Real such that
A6: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> by PASCAL:3;
uf is Element of REAL 3 by A3, EUCLID_8:2;
then uf in REAL 3 ;
then uf in TOP-REAL 3 by EUCLID:22;
then consider t1, t2, t3 being Real such that
A7: uf = <*t1,t2,t3*> by EUCLID_5:1;
reconsider x = t1, y = t2, z = t3 as Element of F_Real by XREAL_0:def 1;
v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> by PASCAL:8, A1, A2, A6, A7;
hence v = MR * ufr by A7, A4, A5, A6, PASCAL:9; :: thesis: verum