let V be finite-dimensional RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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) ; :: thesis: verum

dim V = (dim W1) + (dim W2)

let W1, W2 be Subspace of V; :: thesis: ( 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 ; :: thesis: 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) ; :: thesis: verum