let n, m, k be Nat; :: thesis: for f being n -element real-valued FinSequence
for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real
for g being k -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
let f be n -element real-valued FinSequence; :: thesis: for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real
for g being k -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
A1: len f = n by CARD_1:def 7;
rng f c= REAL ;
then f is FinSequence of REAL by FINSEQ_1:def 4;
then reconsider F = f, n0 = n |-> (In (0,REAL)) as Element of n -tuples_on REAL by A1, FINSEQ_2:92;
let A be Matrix of n,m,F_Real; :: thesis: for B being Matrix of k,m,F_Real
for g being k -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
let B be Matrix of k,m,F_Real; :: thesis: for g being k -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
let g be k -element real-valued FinSequence; :: thesis: (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
A2: len g = k by CARD_1:def 7;
rng g c= REAL ;
then g is FinSequence of REAL by FINSEQ_1:def 4;
then reconsider G = g, k0 = k |-> (In (0,REAL)) as Element of k -tuples_on REAL by A2, FINSEQ_2:92;
f = F + n0 by RVSUM_1:16;
then ( g = G + k0 & f = addreal .: (f,n0) ) by RVSUM_1:16, RVSUM_1:def 4;
then f ^ g = (addreal .: (F,n0)) ^ (addreal .: (k0,G)) by RVSUM_1:def 4
.= addreal .: ((F ^ k0),(n0 ^ G)) by FINSEQOP:11
.= (F ^ k0) + (n0 ^ G) by RVSUM_1:def 4 ;
hence (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran (A ^ B)) . (F ^ k0)) + ((Mx2Tran (A ^ B)) . (n0 ^ G)) by Th22
.= ((Mx2Tran A) . f) + ((Mx2Tran (A ^ B)) . (n0 ^ G)) by Th35
.= ((Mx2Tran A) . f) + ((Mx2Tran B) . g) by Th35 ;
:: thesis: verum