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 holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
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 holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
let A be Matrix of n,m,F_Real; :: thesis: for B being Matrix of k,m,F_Real holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
let B be Matrix of k,m,F_Real; :: thesis: ( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
reconsider k0 = k |-> (In (0,REAL)) as k -element FinSequence of REAL ;
A1: len B = k by MATRIX_0:def 2;
set kf = k0 ^ f;

per cases ( n <> 0 or n = 0 ) ;

suppose A2: n <> 0 ; :: thesis: ( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )

then A3: width A = m by MATRIX13:1;
A4: ( len f = n & len k0 = k ) by CARD_1:def 7;
A5: len A = n by A2, MATRIX13:1;
thus (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f :: thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f

proof

set fk = f ^ k0;

per cases ( k = 0 or k <> 0 ) ;

suppose A6: k = 0 ; :: thesis: (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f

then B is empty by A1;
then A7: Mx2Tran (A ^ B) = Mx2Tran A by A6, FINSEQ_1:34;
k0 is empty by A6;
hence (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f by A7, FINSEQ_1:34; :: thesis: verum

end;

suppose A8: k <> 0 ; :: thesis: (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f

set Mab = Mx2Tran (A ^ B);
set Ma = Mx2Tran A;
A9: width B = m by A8, MATRIX_0:23;

A10: now :: thesis: for i being Nat st 1 <= i & i <= m holds
((Mx2Tran A) . f) . i = ((Mx2Tran (A ^ B)) . (f ^ k0)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= m implies ((Mx2Tran A) . f) . i = ((Mx2Tran (A ^ B)) . (f ^ k0)) . i )
reconsider S1 = Sum (mlt ((@ k0),(Col (B,i)))), S2 = Sum (mlt ((@ f),(Col (A,i)))) as Element of F_Real ;
assume A11: ( 1 <= i & i <= m ) ; :: thesis: ((Mx2Tran A) . f) . i = ((Mx2Tran (A ^ B)) . (f ^ k0)) . i
then A12: i in Seg m ;
mlt ((@ k0),(Col (B,i))) = (0. F_Real) * (Col (B,i)) by A1, FVSUM_1:66
.= k |-> (0. F_Real) by A1, FVSUM_1:58 ;
then A13: Sum (mlt ((@ k0),(Col (B,i)))) = Sum (k |-> 0) by MATRPROB:36
.= 0. F_Real by RVSUM_1:81 ;
A14: ( len (Col (A,i)) = n & len (Col (B,i)) = k ) by A5, A1, MATRIX_0:def 8;
mlt ((@ (f ^ k0)),(Col ((A ^ B),i))) = mlt (((@ f) ^ (@ k0)),((Col (A,i)) ^ (Col (B,i)))) by A3, A9, A12, MATRLIN:26
.= (mlt ((@ f),(Col (A,i)))) ^ (mlt ((@ k0),(Col (B,i)))) by A4, A14, MATRIX14:7 ;
then Sum (mlt ((@ (f ^ k0)),(Col ((A ^ B),i)))) = addreal . ((Sum (mlt ((@ f),(Col (A,i))))),(Sum (mlt ((@ k0),(Col (B,i)))))) by FINSOP_1:5
.= (Sum (mlt ((@ f),(Col (A,i))))) + (Sum (mlt ((@ k0),(Col (B,i))))) by BINOP_2:def 9
.= (@ f) "*" (Col (A,i)) by A13 ;
hence ((Mx2Tran A) . f) . i = (@ (f ^ k0)) "*" (Col ((A ^ B),i)) by A2, A11, Th18
.= ((Mx2Tran (A ^ B)) . (f ^ k0)) . i by A2, A11, Th18 ;
:: thesis: verum

end;

( len ((Mx2Tran (A ^ B)) . (f ^ k0)) = m & len ((Mx2Tran A) . f) = m ) by CARD_1:def 7;
hence (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f by A10; :: thesis: verum

end;

end;

end;

per cases ( k = 0 or k <> 0 ) ;

suppose A15: k = 0 ; :: thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f

then B is empty by A1;
then A16: Mx2Tran (B ^ A) = Mx2Tran A by A15, FINSEQ_1:34;
k0 is empty by A15;
hence (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f by A16, FINSEQ_1:34; :: thesis: verum

end;

suppose A17: k <> 0 ; :: thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f

set Mba = Mx2Tran (B ^ A);
set Ma = Mx2Tran A;
A18: width B = m by A17, MATRIX_0:23;

A19: now :: thesis: for i being Nat st 1 <= i & i <= m holds
((Mx2Tran A) . f) . i = ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= m implies ((Mx2Tran A) . f) . i = ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i )
reconsider S1 = Sum (mlt ((@ k0),(Col (B,i)))), S2 = Sum (mlt ((@ f),(Col (A,i)))) as Element of F_Real ;
assume A20: ( 1 <= i & i <= m ) ; :: thesis: ((Mx2Tran A) . f) . i = ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i
then A21: i in Seg m ;
mlt ((@ k0),(Col (B,i))) = (0. F_Real) * (Col (B,i)) by A1, FVSUM_1:66
.= k |-> (0. F_Real) by A1, FVSUM_1:58 ;
then A22: Sum (mlt ((@ k0),(Col (B,i)))) = Sum (k |-> 0) by MATRPROB:36
.= 0. F_Real by RVSUM_1:81 ;
A23: ( len (Col (A,i)) = n & len (Col (B,i)) = k ) by A5, A1, MATRIX_0:def 8;
mlt ((@ (k0 ^ f)),(Col ((B ^ A),i))) = mlt (((@ k0) ^ (@ f)),((Col (B,i)) ^ (Col (A,i)))) by A3, A18, A21, MATRLIN:26
.= (mlt ((@ k0),(Col (B,i)))) ^ (mlt ((@ f),(Col (A,i)))) by A4, A23, MATRIX14:7 ;
then Sum (mlt ((@ (k0 ^ f)),(Col ((B ^ A),i)))) = addreal . ((Sum (mlt ((@ k0),(Col (B,i))))),(Sum (mlt ((@ f),(Col (A,i)))))) by FINSOP_1:5
.= (Sum (mlt ((@ f),(Col (A,i))))) + (0. F_Real) by A22, BINOP_2:def 9
.= (@ f) "*" (Col (A,i)) ;
hence ((Mx2Tran A) . f) . i = (@ (k0 ^ f)) "*" (Col ((B ^ A),i)) by A2, A20, Th18
.= ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i by A2, A20, Th18 ;
:: thesis: verum

end;

( len ((Mx2Tran (B ^ A)) . (k0 ^ f)) = m & len ((Mx2Tran A) . f) = m ) by CARD_1:def 7;
hence (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f by A19; :: thesis: verum

end;

end;

end;

suppose A24: n = 0 ; :: thesis: ( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )

A25: 0. (TOP-REAL k) = 0* k by EUCLID:70
.= k |-> 0 ;
f = {} by A24;
then A26: ( f ^ (k |-> 0) = k |-> 0 & (k |-> 0) ^ f = k |-> 0 ) by FINSEQ_1:34;
thus (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = 0. (TOP-REAL m) by A25, A26, Th29, A24
.= (Mx2Tran A) . f by A24, Def3 ; :: thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f
thus (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = 0. (TOP-REAL m) by A25, A26, Th29, A24
.= (Mx2Tran A) . f by A24, Def3 ; :: thesis: verum

end;

end;