let X, Y be finite-dimensional RealLinearSpace; ( [:X,Y:] is finite-dimensional & dim [:X,Y:] = (dim X) + (dim Y) )
consider BX being finite Subset of X such that
A1:
BX is Basis of X
by RLVECT_5:def 1;
A2:
card BX = dim X
by A1, RLVECT_5:def 2;
consider BY being finite Subset of Y such that
A3:
BY is Basis of Y
by RLVECT_5:def 1;
reconsider BBX = [:BX,{(0. Y)}:] as Subset of the carrier of [:X,Y:] by ZFMISC_1:96;
reconsider BBY = [:{(0. X)},BY:] as Subset of the carrier of [:X,Y:] by ZFMISC_1:96;
reconsider BBX = BBX as finite Subset of the carrier of [:X,Y:] ;
reconsider BBY = BBY as finite Subset of the carrier of [:X,Y:] ;
reconsider BB = BBX \/ BBY as finite Subset of the carrier of [:X,Y:] ;
BBX /\ BBY = {}
proof
assume
BBX /\ BBY <> {}
;
contradiction
then consider x being
object such that A4:
x in BBX /\ BBY
by XBOOLE_0:def 1;
A5:
(
x in BBX &
x in BBY )
by A4, XBOOLE_0:def 4;
consider a,
b being
object such that A6:
(
a in BX &
b in {(0. Y)} &
x = [a,b] )
by A5, ZFMISC_1:def 2;
consider a1,
b1 being
object such that A7:
(
a1 in {(0. X)} &
b1 in BY &
x = [a1,b1] )
by A5, ZFMISC_1:def 2;
(
a = a1 &
b = b1 )
by A6, A7, XTUPLE_0:1;
then
0. X in BX
by A6, A7, TARSKI:def 1;
hence
contradiction
by Lm1, A1;
verum
end;
then A9: card (BBX \/ BBY) =
(card BBX) + (card BBY)
by CARD_2:40, XBOOLE_0:def 7
.=
(card BX) + (card BBY)
by CARD_1:69
.=
(card BX) + (card [:BY,{(0. X)}:])
by CARD_2:4
.=
(card BX) + (card BY)
by CARD_1:69
;
A10:
BB is Basis of [:X,Y:]
by A1, A3, Th25;
hence A11:
[:X,Y:] is finite-dimensional
by RLVECT_5:def 1; dim [:X,Y:] = (dim X) + (dim Y)
card BB =
(card BX) + (card BY)
by A9
.=
(dim X) + (dim Y)
by A2, RLVECT_5:def 2, A3
;
hence
dim [:X,Y:] = (dim X) + (dim Y)
by A10, A11, RLVECT_5:def 2; verum