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 |-> 0 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 |-> 0 as Element of k -tuples_on REAL by A2, FINSEQ_2:92;
len (n |-> 0) = n by CARD_1:def 7;
then len (n0 ^ G) = n + k by A2, FINSEQ_1:22;
then A3: n0 ^ G is n + k -element by CARD_1:def 7;
len (k |-> 0) = k by CARD_1:def 7;
then len (F ^ k0) = n + k by A1, FINSEQ_1:22;
then A4: F ^ k0 is n + k -element by CARD_1:def 7;
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 A4, A3, Th22
.= ((Mx2Tran A) . f) + ((Mx2Tran (A ^ B)) . (n0 ^ G)) by Th35
.= ((Mx2Tran A) . f) + ((Mx2Tran B) . g) by Th35 ;
:: thesis: verum