let V be finite-dimensional RealLinearSpace; for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
dim V = (dim W1) + (dim W2)
let W1, W2 be Subspace of V; ( V is_the_direct_sum_of W1,W2 implies dim V = (dim W1) + (dim W2) )
assume A1:
V is_the_direct_sum_of W1,W2
; dim V = (dim W1) + (dim W2)
then A2:
RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = W1 + W2
by RLSUB_2:def 4;
W1 /\ W2 = (0). V
by A1, RLSUB_2:def 4;
then (Omega). (W1 /\ W2) =
(0). V
by RLSUB_1:def 4
.=
(0). (W1 /\ W2)
by RLSUB_1:36
;
then
dim (W1 /\ W2) = 0
by Th32;
then (dim W1) + (dim W2) =
(dim (W1 + W2)) + 0
by Th35
.=
dim ((Omega). V)
by A2, RLSUB_1:def 4
.=
dim V
by Th30
;
hence
dim V = (dim W1) + (dim W2)
; verum