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: width (a * A2) = width A2 by MATRIX_3:def 5;
A2: width (a * A1) = width A1 by MATRIX_3:def 5;
then A3: Sum (Width <*(a * A1),(a * A2)*>) = (width A1) + (width A2) by A1, Th20;
A4: len (block_diagonal <*A1,A2*>,a1) = Sum (Len <*A1,A2*>) by Def5;
A5: len (a * A2) = len A2 by MATRIX_3:def 5;
then A6: dom (a * A2) = dom A2 by FINSEQ_3:31;
A7: Sum (Width <*A1,A2*>) = (width A1) + (width A2) by Th20;
A8: Sum (Len <*A1,A2*>) = (len A1) + (len A2) by Th16;
A9: len (a * A1) = len A1 by MATRIX_3:def 5;
then A10: dom (a * A1) = dom A1 by FINSEQ_3:31;

A11: 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 A12: i in dom (a * A1) ; :: thesis: Line (a * (block_diagonal <*A1,A2*>,a1)),i = (Line (a * A1),i) ^ ((width (a * A2)) |-> (a * a1))
then A13: 1 <= i by FINSEQ_3:27;
A14: i <= len A1 by A9, A12, FINSEQ_3:27;
len A1 <= len (block_diagonal <*A1,A2*>,a1) by A8, A4, NAT_1:11;
then i <= len (block_diagonal <*A1,A2*>,a1) by A14, XXREAL_0:2;
hence Line (a * (block_diagonal <*A1,A2*>,a1)),i = a * (Line (block_diagonal <*A1,A2*>,a1),i) by A13, MATRIXR1:20
.= a * ((Line A1,i) ^ ((width A2) |-> a1)) by A10, A12, Th23
.= (a * (Line A1,i)) ^ (a * ((width A2) |-> a1)) by MATRIX15:4
.= (Line (a * A1),i) ^ (a * ((width A2) |-> a1)) by A13, A14, 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 A15: 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 A16: 1 <= i by FINSEQ_3:27;
then A17: 0 + 1 <= i + (len A1) by XREAL_1:9;
A18: i <= len A2 by A5, A15, FINSEQ_3:27;
then i + (len A1) <= len (block_diagonal <*A1,A2*>,a1) by A8, A4, 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 A9, A17, MATRIXR1:20
.= a * (((width A1) |-> a1) ^ (Line A2,i)) by A6, A15, 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 A2, A16, A18, MATRIXR1:20 ;
:: thesis: verum

end;

end;

Sum (Len <*(a * A1),(a * A2)*>) = (len A1) + (len A2) by A9, A5, Th16;
hence a * (block_diagonal <*A1,A2*>,a1) = block_diagonal <*(a * A1),(a * A2)*>,(a * a1) by A8, A3, A7, A11, Th23; :: thesis: verum