let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let b2 be OrdBasis of V2; :: thesis: for f being linear-transformation of V1,V2
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let f be linear-transformation of V1,V2; :: thesis: for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let W1, W2 be Subspace of V1; :: thesis: for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let U1, U2 be Subspace of V2; :: thesis: ( ( dim W1 = 0 implies dim U1 = 0 ) & ( dim W2 = 0 implies dim U2 = 0 ) & V2 is_the_direct_sum_of U1,U2 implies for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K) )
assume that
A1: ( dim W1 = 0 implies dim U1 = 0 ) and
A2: ( dim W2 = 0 implies dim U2 = 0 ) and
A3: V2 is_the_direct_sum_of U1,U2 ; :: thesis: for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
A4: U1 /\ U2 = (0). V2 by A3, VECTSP_5:def 4;
A5: U1 + U2 = (Omega). V2 by A3, VECTSP_5:def 4;
let fW1 be linear-transformation of W1,U1; :: thesis: for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let fW2 be linear-transformation of W2,U2; :: thesis: ( fW1 = f | W1 & fW2 = f | W2 implies for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K) )
assume that
A6: fW1 = f | W1 and
A7: fW2 = f | W2 ; :: thesis: for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let w1 be OrdBasis of W1; :: thesis: for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let w2 be OrdBasis of W2; :: thesis: for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let u1 be OrdBasis of U1; :: thesis: for u2 being OrdBasis of U2 st w1 ^ w2 = b1 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
let u2 be OrdBasis of U2; :: thesis: ( w1 ^ w2 = b1 & u1 ^ u2 = b2 implies AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K) )
assume that
A8: w1 ^ w2 = b1 and
A9: u1 ^ u2 = b2 ; :: thesis: AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)
set A1 = AutMt fW1,w1,u1;
set A2 = AutMt fW2,w2,u2;
set A12 = <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>;
set A = AutMt f,b1,b2;
( len w1 = dim W1 & len w2 = dim W2 & len u1 = dim U1 & len u2 = dim U2 ) by Th21;
then A10: ( len b1 = (len w1) + (len w2) & len b2 = (len u1) + (len u2) & len w1 = len (AutMt fW1,w1,u1) & len w2 = len (AutMt fW2,w2,u2) & len b1 = len (AutMt f,b1,b2) & len u1 = width (AutMt fW1,w1,u1) & len u2 = width (AutMt fW2,w2,u2) ) by A1, A2, A8, A9, FINSEQ_1:35, MATRIX13:1, MATRLIN:def 10;
A11: ( Sum (Len <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>) = (len (AutMt fW1,w1,u1)) + (len (AutMt fW2,w2,u2)) & Sum (Width <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>) = (width (AutMt fW1,w1,u1)) + (width (AutMt fW2,w2,u2)) ) by MATRIXJ1:16, MATRIXJ1:20;

now

let i be Nat; :: thesis: ( ( i in dom (AutMt fW1,w1,u1) implies Line (AutMt f,b1,b2),i = (Line (AutMt fW1,w1,u1),i) ^ ((width (AutMt fW2,w2,u2)) |-> (0. K)) ) & ( i in dom (AutMt fW2,w2,u2) implies Line (AutMt f,b1,b2),(i + (len (AutMt fW1,w1,u1))) = ((width (AutMt fW1,w1,u1)) |-> (0. K)) ^ (Line (AutMt fW2,w2,u2),i) ) )
A12: ( dom (AutMt f,b1,b2) = Seg (len (AutMt f,b1,b2)) & dom (AutMt f,b1,b2) = dom b1 & dom (AutMt fW1,w1,u1) = dom w1 & dom (AutMt fW2,w2,u2) = dom w2 ) by A10, FINSEQ_1:def 3, FINSEQ_3:31;
A13: ( dom fW1 = the carrier of W1 & dom fW2 = the carrier of W2 ) by FUNCT_2:def 1;
reconsider uu = u1 ^ u2 as OrdBasis of U1 + U2 by A4, Th26;
reconsider fb = f . (b1 /. i), fbi = f . (b1 /. (i + (len (AutMt fW1,w1,u1)))) as Vector of (U1 + U2) by A5;
thus ( i in dom (AutMt fW1,w1,u1) implies Line (AutMt f,b1,b2),i = (Line (AutMt fW1,w1,u1),i) ^ ((width (AutMt fW2,w2,u2)) |-> (0. K)) ) :: thesis: ( i in dom (AutMt fW2,w2,u2) implies Line (AutMt f,b1,b2),(i + (len (AutMt fW1,w1,u1))) = ((width (AutMt fW1,w1,u1)) |-> (0. K)) ^ (Line (AutMt fW2,w2,u2),i) )

proof

assume A14: i in dom (AutMt fW1,w1,u1) ; :: thesis: Line (AutMt f,b1,b2),i = (Line (AutMt fW1,w1,u1),i) ^ ((width (AutMt fW2,w2,u2)) |-> (0. K))
len (AutMt fW1,w1,u1) <= len (AutMt f,b1,b2) by A10, NAT_1:11;
then A15: ( dom (AutMt fW1,w1,u1) = Seg (len (AutMt fW1,w1,u1)) & Seg (len (AutMt fW1,w1,u1)) c= Seg (len (AutMt f,b1,b2)) ) by FINSEQ_1:7, FINSEQ_1:def 3;
then b1 /. i = b1 . i by A12, A14, PARTFUN1:def 8
.= w1 . i by A8, A12, A14, FINSEQ_1:def 7
.= w1 /. i by A12, A14, PARTFUN1:def 8 ;
then A16: fb = fW1 . (w1 /. i) by A6, A13, FUNCT_1:70;
A17: Line (AutMt fW1,w1,u1),i = (AutMt fW1,w1,u1) . i by A10, A14, A15, MATRIX_2:10
.= (AutMt fW1,w1,u1) /. i by A14, PARTFUN1:def 8
.= (fW1 . (w1 /. i)) |-- u1 by A12, A14, MATRLIN:def 10 ;
thus Line (AutMt f,b1,b2),i = (AutMt f,b1,b2) . i by A10, A14, A15, MATRIX_2:10
.= (AutMt f,b1,b2) /. i by A12, A14, A15, PARTFUN1:def 8
.= (f . (b1 /. i)) |-- b2 by A12, A14, A15, MATRLIN:def 10
.= fb |-- uu by A5, A9, Th25
.= (fb + (0. (U1 + U2))) |-- uu by RLVECT_1:def 7
.= ((fW1 . (w1 /. i)) |-- u1) ^ ((0. U2) |-- u2) by A4, A16, Th24, VECTSP_4:20
.= (Line (AutMt fW1,w1,u1),i) ^ ((width (AutMt fW2,w2,u2)) |-> (0. K)) by A10, A17, Th20 ; :: thesis: verum

end;

thus ( i in dom (AutMt fW2,w2,u2) implies Line (AutMt f,b1,b2),(i + (len (AutMt fW1,w1,u1))) = ((width (AutMt fW1,w1,u1)) |-> (0. K)) ^ (Line (AutMt fW2,w2,u2),i) ) :: thesis: verum

proof

assume A18: i in dom (AutMt fW2,w2,u2) ; :: thesis: Line (AutMt f,b1,b2),(i + (len (AutMt fW1,w1,u1))) = ((width (AutMt fW1,w1,u1)) |-> (0. K)) ^ (Line (AutMt fW2,w2,u2),i)
A19: dom (AutMt fW2,w2,u2) = Seg (len (AutMt fW2,w2,u2)) by FINSEQ_1:def 3;
then A20: i + (len (AutMt fW1,w1,u1)) in dom (AutMt f,b1,b2) by A10, A18, A12, FINSEQ_1:81;
b1 /. (i + (len (AutMt fW1,w1,u1))) = b1 . (i + (len (AutMt fW1,w1,u1))) by A12, A19, A10, A18, FINSEQ_1:81, PARTFUN1:def 8
.= w2 . i by A10, A18, A8, A12, FINSEQ_1:def 7
.= w2 /. i by A12, A18, PARTFUN1:def 8 ;
then A21: fbi = fW2 . (w2 /. i) by A7, A13, FUNCT_1:70;
A22: Line (AutMt fW2,w2,u2),i = (AutMt fW2,w2,u2) . i by A19, A10, A18, MATRIX_2:10
.= (AutMt fW2,w2,u2) /. i by A18, PARTFUN1:def 8
.= (fW2 . (w2 /. i)) |-- u2 by A12, A18, MATRLIN:def 10 ;
thus Line (AutMt f,b1,b2),(i + (len (AutMt fW1,w1,u1))) = (AutMt f,b1,b2) . (i + (len (AutMt fW1,w1,u1))) by A10, A19, A18, A12, FINSEQ_1:81, MATRIX_2:10
.= (AutMt f,b1,b2) /. (i + (len (AutMt fW1,w1,u1))) by A19, A10, A18, A12, FINSEQ_1:81, PARTFUN1:def 8
.= (f . (b1 /. (i + (len (AutMt fW1,w1,u1))))) |-- b2 by A12, A20, MATRLIN:def 10
.= fbi |-- uu by A5, A9, Th25
.= ((0. (U1 + U2)) + fbi) |-- uu by RLVECT_1:def 7
.= ((0. U1) |-- u1) ^ ((fW2 . (w2 /. i)) |-- u2) by A4, A21, Th24, VECTSP_4:20
.= ((width (AutMt fW1,w1,u1)) |-> (0. K)) ^ (Line (AutMt fW2,w2,u2),i) by A10, A22, Th20 ; :: thesis: verum

end;

end;

hence AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K) by A10, A11, MATRIXJ1:23; :: thesis: verum