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:29;
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:29;

A11: now :: thesis: for i being Nat holds
( ( 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)) ) )

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:25;
A14: i <= len A1 by A9, A12, FINSEQ_3:25;
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:53 ;
:: 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:25;
then A17: 0 + 1 <= i + (len A1) by XREAL_1:7;
A18: i <= len A2 by A5, A15, FINSEQ_3:25;
then i + (len A1) <= len (block_diagonal (<*A1,A2*>,a1)) by A8, A4, XREAL_1:7;
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:53
.= ((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