let K be Field; :: thesis: for a, a1 being Element of K
for G being FinSequence_of_Matrix of K holds a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
let a, a1 be Element of K; :: thesis: for G being FinSequence_of_Matrix of K holds a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
let G be FinSequence_of_Matrix of K; :: thesis: a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
defpred S₁[ Nat] means for a, a1 being Element of K
for G being FinSequence_of_Matrix of K st len G = $1 holds
a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1));
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let a, a1 be Element of K; :: thesis: for G being FinSequence_of_Matrix of K st len G = n + 1 holds
a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
let G be FinSequence_of_Matrix of K; :: thesis: ( len G = n + 1 implies a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1)) )
assume A3: len G = n + 1 ; :: thesis: a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
A4: G = (G | n) ^ <*(G . (n + 1))*> by A3, FINSEQ_3:55;
n <= n + 1 by NAT_1:13;
then A5: len (G | n) = n by A3, FINSEQ_1:59;
1 in Seg 1 ;
then 1 in dom <*a*> by FINSEQ_1:def 8;
then A6: <*a*> . 1 = <*a*> /. 1 by PARTFUN1:def 6;
A8: len <*a*> = 1 by FINSEQ_1:39;
A9: len <*(G . (n + 1))*> = 1 by FINSEQ_1:39;
A10: len (n |-> a) = n by CARD_1:def 7;
(n + 1) |-> a = (n |-> a) ^ <*a*> by FINSEQ_2:60;
hence block_diagonal ((mlt (((len G) |-> a),G)),(a * a1)) = block_diagonal (((mlt ((n |-> a),(G | n))) ^ (mlt (<*a*>,<*(G . (n + 1))*>))),(a * a1)) by A3, A4, A5, A10, A9, A8, Th64
.= block_diagonal (((mlt ((n |-> a),(G | n))) ^ <*(a * (G . (n + 1)))*>),(a * a1)) by A6, Th63
.= block_diagonal ((<*(block_diagonal ((mlt ((n |-> a),(G | n))),(a * a1)))*> ^ <*(a * (G . (n + 1)))*>),(a * a1)) by Th35
.= block_diagonal (<*(a * (block_diagonal ((G | n),a1))),(a * (G . (n + 1)))*>,(a * a1)) by A2, A5
.= a * (block_diagonal (<*(block_diagonal ((G | n),a1)),(G . (n + 1))*>,a1)) by Lm7
.= a * (block_diagonal (G,a1)) by A4, Th35 ;
:: thesis: verum

end;

A11: S₁[ 0 ]

proof

let a, a1 be Element of K; :: thesis: for G being FinSequence_of_Matrix of K st len G = 0 holds
a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
let G be FinSequence_of_Matrix of K; :: thesis: ( len G = 0 implies a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1)) )
assume A12: len G = 0 ; :: thesis: a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
dom (mlt (((len G) |-> a),G)) = dom G by Def9;
then len (mlt (((len G) |-> a),G)) = len G by FINSEQ_3:29;
then Len (mlt (((len G) |-> a),G)) = {} by A12;
then len (block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))) = 0 by Def5, RVSUM_1:72;
then A13: block_diagonal ((mlt (((len G) |-> a),G)),(a * a1)) = {} ;
Len G = {} by A12;
then len (block_diagonal (G,a1)) = 0 by Def5, RVSUM_1:72;
then len (a * (block_diagonal (G,a1))) = 0 by MATRIX_3:def 5;
hence a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1)) by A13; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A1);
hence a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1)) ; :: thesis: verum