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;
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
A5: fW1 = f | W1 and
A6: 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
A7: w1 ^ w2 = b1 and
A8: u1 ^ u2 = b2 ; :: thesis: AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
A9: len b1 = (len w1) + (len w2) by A7, FINSEQ_1:22;
A10: U1 + U2 = (Omega). V2 by A3, VECTSP_5:def 4;
set A = AutMt (f,b1,b2);
A11: len b1 = len (AutMt (f,b1,b2)) by MATRLIN:def 8;
set A2 = AutMt (fW2,w2,u2);
A12: ( len w2 = dim W2 & len u2 = dim U2 ) by Th21;
then A13: len w2 = len (AutMt (fW2,w2,u2)) by A2, MATRIX13:1;
set A1 = AutMt (fW1,w1,u1);
A14: ( len w1 = dim W1 & len u1 = dim U1 ) by Th21;
then A15: len w1 = len (AutMt (fW1,w1,u1)) by A1, MATRIX13:1;
A16: len u2 = width (AutMt (fW2,w2,u2)) by A2, A12, MATRIX13:1;
A17: len u1 = width (AutMt (fW1,w1,u1)) by A1, A14, MATRIX13:1;

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

reconsider uu = u1 ^ u2 as OrdBasis of U1 + U2 by A4, Th26;
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)) ) )
A19: dom (AutMt (f,b1,b2)) = Seg (len (AutMt (f,b1,b2))) by FINSEQ_1:def 3;
reconsider fb = f . (b1 /. i), fbi = f . (b1 /. (i + (len (AutMt (fW1,w1,u1))))) as Vector of (U1 + U2) by A10;
A20: dom (AutMt (f,b1,b2)) = dom b1 by A11, FINSEQ_3:29;
A21: dom (AutMt (fW1,w1,u1)) = dom w1 by A15, FINSEQ_3:29;
A22: dom fW1 = the carrier of W1 by FUNCT_2:def 1;
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 A23: 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))
A24: dom (AutMt (fW1,w1,u1)) = Seg (len (AutMt (fW1,w1,u1))) by FINSEQ_1:def 3;
then A25: Line ((AutMt (fW1,w1,u1)),i) = (AutMt (fW1,w1,u1)) . i by A15, A23, MATRIX_0:52
.= (AutMt (fW1,w1,u1)) /. i by A23, PARTFUN1:def 6
.= (fW1 . (w1 /. i)) |-- u1 by A21, A23, MATRLIN:def 8 ;
len (AutMt (fW1,w1,u1)) <= len (AutMt (f,b1,b2)) by A9, A15, A11, NAT_1:11;
then A26: Seg (len (AutMt (fW1,w1,u1))) c= Seg (len (AutMt (f,b1,b2))) by FINSEQ_1:5;
then b1 /. i = b1 . i by A19, A20, A23, A24, PARTFUN1:def 6
.= w1 . i by A7, A21, A23, FINSEQ_1:def 7
.= w1 /. i by A21, A23, PARTFUN1:def 6 ;
then A27: fb = fW1 . (w1 /. i) by A5, A22, FUNCT_1:47;
thus Line ((AutMt (f,b1,b2)),i) = (AutMt (f,b1,b2)) . i by A11, A23, A24, A26, MATRIX_0:52
.= (AutMt (f,b1,b2)) /. i by A19, A23, A24, A26, PARTFUN1:def 6
.= (f . (b1 /. i)) |-- b2 by A19, A20, A23, A24, A26, MATRLIN:def 8
.= fb |-- uu by A10, A8, Th25
.= (fb + (0. (U1 + U2))) |-- uu by RLVECT_1:def 4
.= ((fW1 . (w1 /. i)) |-- u1) ^ ((0. U2) |-- u2) by A4, A27, Th24, VECTSP_4:12
.= (Line ((AutMt (fW1,w1,u1)),i)) ^ ((width (AutMt (fW2,w2,u2))) |-> (0. K)) by A16, A25, Th20 ; :: thesis: verum

end;

A28: dom (AutMt (fW2,w2,u2)) = dom w2 by A13, FINSEQ_3:29;
A29: dom fW2 = the carrier of W2 by FUNCT_2:def 1;
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 A30: 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))
A31: dom (AutMt (fW2,w2,u2)) = Seg (len (AutMt (fW2,w2,u2))) by FINSEQ_1:def 3;
then A32: i + (len (AutMt (fW1,w1,u1))) in dom (AutMt (f,b1,b2)) by A9, A15, A13, A11, A19, A30, FINSEQ_1:60;
b1 /. (i + (len (AutMt (fW1,w1,u1)))) = b1 . (i + (len (AutMt (fW1,w1,u1)))) by A9, A15, A13, A11, A19, A20, A30, A31, FINSEQ_1:60, PARTFUN1:def 6
.= w2 . i by A7, A15, A28, A30, FINSEQ_1:def 7
.= w2 /. i by A28, A30, PARTFUN1:def 6 ;
then A33: fbi = fW2 . (w2 /. i) by A6, A29, FUNCT_1:47;
A34: Line ((AutMt (fW2,w2,u2)),i) = (AutMt (fW2,w2,u2)) . i by A13, A30, A31, MATRIX_0:52
.= (AutMt (fW2,w2,u2)) /. i by A30, PARTFUN1:def 6
.= (fW2 . (w2 /. i)) |-- u2 by A28, A30, MATRLIN:def 8 ;
thus Line ((AutMt (f,b1,b2)),(i + (len (AutMt (fW1,w1,u1))))) = (AutMt (f,b1,b2)) . (i + (len (AutMt (fW1,w1,u1)))) by A9, A15, A13, A11, A19, A30, A31, FINSEQ_1:60, MATRIX_0:52
.= (AutMt (f,b1,b2)) /. (i + (len (AutMt (fW1,w1,u1)))) by A9, A15, A13, A11, A19, A30, A31, FINSEQ_1:60, PARTFUN1:def 6
.= (f . (b1 /. (i + (len (AutMt (fW1,w1,u1)))))) |-- b2 by A20, A32, MATRLIN:def 8
.= fbi |-- uu by A10, A8, Th25
.= ((0. (U1 + U2)) + fbi) |-- uu by RLVECT_1:def 4
.= ((0. U1) |-- u1) ^ ((fW2 . (w2 /. i)) |-- u2) by A4, A33, Th24, VECTSP_4:12
.= ((width (AutMt (fW1,w1,u1))) |-> (0. K)) ^ (Line ((AutMt (fW2,w2,u2)),i)) by A17, A34, Th20 ; :: thesis: verum

end;

end;

set A12 = <*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>;
A35: ( 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;
len b2 = (len u1) + (len u2) by A8, FINSEQ_1:22;
hence AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K)) by A9, A15, A13, A17, A16, A35, A18, MATRIXJ1:23; :: thesis: verum