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:61;
n <= n + 1 by NAT_1:13;
then A5: len (G | n) = n by A3, FINSEQ_1:80;
1 in Seg 1 ;
then 1 in dom <*a*> by FINSEQ_1:def 8;
then A6: <*a*> . 1 = <*a*> /. 1 by PARTFUN1:def 8;
A7: <*a*> . 1 = a by FINSEQ_1:def 8;
A8: len <*a*> = 1 by FINSEQ_1:56;
A9: len <*(G . (n + 1))*> = 1 by FINSEQ_1:56;
A10: len (n |-> a) = n by FINSEQ_1:def 18;
(n + 1) |-> a = (n |-> a) ^ <*a*> by FINSEQ_2:74;
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, A7, 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
set M = mlt ((len G) |-> a),G;

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:31;
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:102;
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:102;
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