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:35;
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 10;
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

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:31;
A21: dom (AutMt fW1,w1,u1) = dom w1 by A15, FINSEQ_3:31;
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_2:10
.= (AutMt fW1,w1,u1) /. i by A23, PARTFUN1:def 8
.= (fW1 . (w1 /. i)) |-- u1 by A21, A23, MATRLIN:def 10 ;
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:7;
then b1 /. i = b1 . i by A19, A20, A23, A24, PARTFUN1:def 8
.= w1 . i by A7, A21, A23, FINSEQ_1:def 7
.= w1 /. i by A21, A23, PARTFUN1:def 8 ;
then A27: fb = fW1 . (w1 /. i) by A5, A22, FUNCT_1:70;
thus Line (AutMt f,b1,b2),i = (AutMt f,b1,b2) . i by A11, A23, A24, A26, MATRIX_2:10
.= (AutMt f,b1,b2) /. i by A19, A23, A24, A26, PARTFUN1:def 8
.= (f . (b1 /. i)) |-- b2 by A19, A20, A23, A24, A26, MATRLIN:def 10
.= fb |-- uu by A10, A8, Th25
.= (fb + (0. (U1 + U2))) |-- uu by RLVECT_1:def 7
.= ((fW1 . (w1 /. i)) |-- u1) ^ ((0. U2) |-- u2) by A4, A27, Th24, VECTSP_4:20
.= (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:31;
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:81;
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:81, PARTFUN1:def 8
.= w2 . i by A7, A15, A28, A30, FINSEQ_1:def 7
.= w2 /. i by A28, A30, PARTFUN1:def 8 ;
then A33: fbi = fW2 . (w2 /. i) by A6, A29, FUNCT_1:70;
A34: Line (AutMt fW2,w2,u2),i = (AutMt fW2,w2,u2) . i by A13, A30, A31, MATRIX_2:10
.= (AutMt fW2,w2,u2) /. i by A30, PARTFUN1:def 8
.= (fW2 . (w2 /. i)) |-- u2 by A28, A30, 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 A9, A15, A13, A11, A19, A30, A31, FINSEQ_1:81, MATRIX_2:10
.= (AutMt f,b1,b2) /. (i + (len (AutMt fW1,w1,u1))) by A9, A15, A13, A11, A19, A30, A31, FINSEQ_1:81, PARTFUN1:def 8
.= (f . (b1 /. (i + (len (AutMt fW1,w1,u1))))) |-- b2 by A20, A32, MATRLIN:def 10
.= fbi |-- uu by A10, A8, Th25
.= ((0. (U1 + U2)) + fbi) |-- uu by RLVECT_1:def 7
.= ((0. U1) |-- u1) ^ ((fW2 . (w2 /. i)) |-- u2) by A4, A33, Th24, VECTSP_4:20
.= ((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:35;
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