let K be Field; :: thesis: for a, a1 being Element of K
for A1, A2 being Matrix of K holds a * (block_diagonal <*A1,A2*>,a1) = block_diagonal <*(a * A1),(a * A2)*>,(a * a1)
let a, a1 be Element of K; :: thesis: for A1, A2 being Matrix of K holds a * (block_diagonal <*A1,A2*>,a1) = block_diagonal <*(a * A1),(a * A2)*>,(a * a1)
let A1, A2 be Matrix of K; :: thesis: a * (block_diagonal <*A1,A2*>,a1) = block_diagonal <*(a * A1),(a * A2)*>,(a * a1)
set AA1 = a * A1;
set AA2 = a * A2;
set aa1 = a * a1;
set B = block_diagonal <*A1,A2*>,a1;
A1: ( len (a * A1) = len A1 & width (a * A1) = width A1 & len (a * A2) = len A2 & width (a * A2) = width A2 ) by MATRIX_3:def 5;
then A2: ( Sum (Len <*(a * A1),(a * A2)*>) = (len A1) + (len A2) & Sum (Len <*A1,A2*>) = (len A1) + (len A2) & Sum (Width <*(a * A1),(a * A2)*>) = (width A1) + (width A2) & Sum (Width <*A1,A2*>) = (width A1) + (width A2) & len (block_diagonal <*A1,A2*>,a1) = Sum (Len <*A1,A2*>) ) by Th16, Th20, Def5;
A3: ( dom (a * A1) = dom A1 & dom (a * A2) = dom A2 ) by A1, FINSEQ_3:31;

now

let i be Nat; :: thesis: ( ( i in dom (a * A1) implies Line (a * (block_diagonal <*A1,A2*>,a1)),i = (Line (a * A1),i) ^ ((width (a * A2)) |-> (a * a1)) ) & ( i in dom (a * A2) implies Line (a * (block_diagonal <*A1,A2*>,a1)),(i + (len (a * A1))) = ((width (a * A1)) |-> (a * a1)) ^ (Line (a * A2),i) ) )
thus ( i in dom (a * A1) implies Line (a * (block_diagonal <*A1,A2*>,a1)),i = (Line (a * A1),i) ^ ((width (a * A2)) |-> (a * a1)) ) :: thesis: ( i in dom (a * A2) implies Line (a * (block_diagonal <*A1,A2*>,a1)),(i + (len (a * A1))) = ((width (a * A1)) |-> (a * a1)) ^ (Line (a * A2),i) )

proof

assume A4: i in dom (a * A1) ; :: thesis: Line (a * (block_diagonal <*A1,A2*>,a1)),i = (Line (a * A1),i) ^ ((width (a * A2)) |-> (a * a1))
then A5: ( 1 <= i & i <= len A1 & len A1 <= len (block_diagonal <*A1,A2*>,a1) ) by A2, A1, FINSEQ_3:27, NAT_1:11;
then i <= len (block_diagonal <*A1,A2*>,a1) by XXREAL_0:2;
hence Line (a * (block_diagonal <*A1,A2*>,a1)),i = a * (Line (block_diagonal <*A1,A2*>,a1),i) by A5, MATRIXR1:20
.= a * ((Line A1,i) ^ ((width A2) |-> a1)) by A3, A4, Th23
.= (a * (Line A1,i)) ^ (a * ((width A2) |-> a1)) by MATRIX15:4
.= (Line (a * A1),i) ^ (a * ((width A2) |-> a1)) by A5, MATRIXR1:20
.= (Line (a * A1),i) ^ ((width (a * A2)) |-> (a * a1)) by A1, FVSUM_1:66 ;
:: thesis: verum

end;

thus ( i in dom (a * A2) implies Line (a * (block_diagonal <*A1,A2*>,a1)),(i + (len (a * A1))) = ((width (a * A1)) |-> (a * a1)) ^ (Line (a * A2),i) ) :: thesis: verum

proof

assume A6: i in dom (a * A2) ; :: thesis: Line (a * (block_diagonal <*A1,A2*>,a1)),(i + (len (a * A1))) = ((width (a * A1)) |-> (a * a1)) ^ (Line (a * A2),i)
then A7: ( 1 <= i & i <= len A2 ) by A1, FINSEQ_3:27;
then ( 0 + 1 <= i + (len A1) & i + (len A1) <= len (block_diagonal <*A1,A2*>,a1) ) by A2, XREAL_1:9;
hence Line (a * (block_diagonal <*A1,A2*>,a1)),(i + (len (a * A1))) = a * (Line (block_diagonal <*A1,A2*>,a1),(i + (len A1))) by A1, MATRIXR1:20
.= a * (((width A1) |-> a1) ^ (Line A2,i)) by A3, A6, Th23
.= (a * ((width A1) |-> a1)) ^ (a * (Line A2,i)) by MATRIX15:4
.= ((width A1) |-> (a * a1)) ^ (a * (Line A2,i)) by FVSUM_1:66
.= ((width (a * A1)) |-> (a * a1)) ^ (Line (a * A2),i) by A1, A7, MATRIXR1:20 ;
:: thesis: verum

end;

end;

hence a * (block_diagonal <*A1,A2*>,a1) = block_diagonal <*(a * A1),(a * A2)*>,(a * a1) by A2, Th23; :: thesis: verum