let n, k, m be Nat; :: thesis: for f being n -element real-valued FinSequence
for A being Matrix of n,k,F_Real
for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
let f be n -element real-valued FinSequence; :: thesis: for A being Matrix of n,k,F_Real
for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
let A be Matrix of n,k,F_Real; :: thesis: for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
let B be Matrix of n,m,F_Real; :: thesis: ( ( n = 0 implies k + m = 0 ) implies (Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f) )
set L = LineVec2Mx (@ f);
set MAB = (Mx2Tran (A ^^ B)) . f;
set MA = (Mx2Tran A) . f;
set MB = (Mx2Tran B) . f;
A1: len ((Mx2Tran A) . f) = k by CARD_1:def 7;
assume A2: ( n = 0 implies k + m = 0 ) ; :: thesis: (Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
then ( n = 0 implies k = 0 ) ;
then A3: width A = k by MATRIX13:1;
( n = 0 implies m = 0 ) by A2;
then A4: width B = m by MATRIX13:1;
A5: len ((Mx2Tran B) . f) = m by CARD_1:def 7;
then A6: len (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) = k + m by A1, FINSEQ_1:22;
A7: for i being Nat st 1 <= i & i <= k + m holds
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= k + m implies (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i )
assume that
A8: 1 <= i and
A9: i <= k + m ; :: thesis: (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i
A10: i in dom (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) by A6, A8, A9, FINSEQ_3:25;
A11: ((Mx2Tran (A ^^ B)) . f) . i = (@ f) "*" (Col ((A ^^ B),i)) by A2, A3, A4, A8, A9, Th18;

per cases ( i in dom ((Mx2Tran A) . f) or ex j being Nat st
( j in dom ((Mx2Tran B) . f) & i = (len ((Mx2Tran A) . f)) + j ) ) by A10, FINSEQ_1:25;

suppose A12: i in dom ((Mx2Tran A) . f) ; :: thesis: (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i

then i <= k by A1, FINSEQ_3:25;
then A13: ((Mx2Tran A) . f) . i = (@ f) "*" (Col (A,i)) by A2, A8, Th18;
( i in Seg (width A) & (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran A) . f) . i ) by A3, A1, A12, FINSEQ_1:def 3, FINSEQ_1:def 7;
hence (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i by A11, A13, MATRIX15:16; :: thesis: verum

end;

suppose ex j being Nat st
( j in dom ((Mx2Tran B) . f) & i = (len ((Mx2Tran A) . f)) + j ) ; :: thesis: (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i

then consider j being Nat such that
A14: j in dom ((Mx2Tran B) . f) and
A15: i = (len ((Mx2Tran A) . f)) + j ;
( 1 <= j & j <= m ) by A5, A14, FINSEQ_3:25;
then A16: ((Mx2Tran B) . f) . j = (@ f) "*" (Col (B,j)) by A2, Th18;
( j in Seg (width B) & (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran B) . f) . j ) by A4, A5, A14, A15, FINSEQ_1:def 3, FINSEQ_1:def 7;
hence (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i by A3, A1, A11, A15, A16, MATRIX15:17; :: thesis: verum

end;

end;

end;

len ((Mx2Tran (A ^^ B)) . f) = k + m by A3, A4, CARD_1:def 7;
hence (Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f) by A6, A7, FINSEQ_1:14; :: thesis: verum