let X, Y be RealLinearSpace; :: thesis: for X1 being Subspace of X
for Y1 being Subspace of Y holds [:X1,Y1:] is Subspace of [:X,Y:]
let X1 be Subspace of X; :: thesis: for Y1 being Subspace of Y holds [:X1,Y1:] is Subspace of [:X,Y:]
let Y1 be Subspace of Y; :: thesis: [:X1,Y1:] is Subspace of [:X,Y:]
set V = [:X,Y:];
set XY1 = [:X1,Y1:];
A1: ( the carrier of X1 c= the carrier of X & 0. X1 = 0. X & the addF of X1 = the addF of X || the carrier of X1 & the Mult of X1 = the Mult of X | [:REAL, the carrier of X1:] ) by RLSUB_1:def 2;
A2: ( the carrier of Y1 c= the carrier of Y & 0. Y1 = 0. Y & the addF of Y1 = the addF of Y || the carrier of Y1 & the Mult of Y1 = the Mult of Y | [:REAL, the carrier of Y1:] ) by RLSUB_1:def 2;
A3: the carrier of [:X1,Y1:] c= the carrier of [:X,Y:] by A1, A2, ZFMISC_1:96;
A4: 0. [:X1,Y1:] = [(0. X),(0. Y)] by A2, RLSUB_1:def 2
.= 0. [:X,Y:] ;
set f = the addF of [:X1,Y1:];
set g = the addF of [:X,Y:] || the carrier of [:X1,Y1:];
A5: dom the addF of [:X,Y:] = [: the carrier of [:X,Y:], the carrier of [:X,Y:]:] by FUNCT_2:def 1;
A6: dom ( the addF of [:X,Y:] || the carrier of [:X1,Y1:]) = [: the carrier of [:X1,Y1:], the carrier of [:X1,Y1:]:] by A3, A5, RELAT_1:62, ZFMISC_1:96;
A7: dom the addF of [:X1,Y1:] = [: the carrier of [:X1,Y1:], the carrier of [:X1,Y1:]:] by FUNCT_2:def 1;
for z being object st z in dom the addF of [:X1,Y1:] holds
the addF of [:X1,Y1:] . z = ( the addF of [:X,Y:] || the carrier of [:X1,Y1:]) . z

proof

let z be object ; :: thesis: ( z in dom the addF of [:X1,Y1:] implies the addF of [:X1,Y1:] . z = ( the addF of [:X,Y:] || the carrier of [:X1,Y1:]) . z )
assume z in dom the addF of [:X1,Y1:] ; :: thesis: the addF of [:X1,Y1:] . z = ( the addF of [:X,Y:] || the carrier of [:X1,Y1:]) . z
then consider x, y being object such that
A8: ( x in the carrier of [:X1,Y1:] & y in the carrier of [:X1,Y1:] & z = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x, y = y as Point of [:X1,Y1:] by A8;
consider ax being Point of X1, bx being Point of Y1 such that
A9: x = [ax,bx] by PRVECT_3:9;
consider az being Point of X1, bz being Point of Y1 such that
A10: y = [az,bz] by PRVECT_3:9;
reconsider ax0 = ax, az0 = az as Point of X by A1;
reconsider bx0 = bx, bz0 = bz as Point of Y by A2;
reconsider x1 = [ax0,bx0] as Point of [:X,Y:] ;
reconsider y1 = [az0,bz0] as Point of [:X,Y:] ;
A11: bx + bz = bx0 + bz0 by RLSUB_1:13;
thus the addF of [:X1,Y1:] . z = the addF of [:X1,Y1:] . (x,y) by A8
.= x + y
.= [(ax + az),(bx + bz)] by A9, A10, PRVECT_3:9
.= [(ax0 + az0),(bx0 + bz0)] by A11, RLSUB_1:13
.= x1 + y1 by PRVECT_3:9
.= ( the addF of [:X,Y:] || the carrier of [:X1,Y1:]) . [x1,y1] by A9, A10, FUNCT_1:49, ZFMISC_1:87
.= ( the addF of [:X,Y:] || the carrier of [:X1,Y1:]) . z by A8, A9, A10 ; :: thesis: verum

end;

then A12: the addF of [:X1,Y1:] = the addF of [:X,Y:] || the carrier of [:X1,Y1:] by A6, A7, FUNCT_1:2;
set f = the Mult of [:X1,Y1:];
set g = the Mult of [:X,Y:] | [:REAL, the carrier of [:X1,Y1:]:];
A13: dom the Mult of [:X,Y:] = [:REAL, the carrier of [:X,Y:]:] by FUNCT_2:def 1;
A14: dom ( the Mult of [:X,Y:] | [:REAL, the carrier of [:X1,Y1:]:]) = [:REAL, the carrier of [:X1,Y1:]:] by A3, A13, RELAT_1:62, ZFMISC_1:96;
A15: dom the Mult of [:X1,Y1:] = [:REAL, the carrier of [:X1,Y1:]:] by FUNCT_2:def 1;
for z being object st z in dom the Mult of [:X1,Y1:] holds
the Mult of [:X1,Y1:] . z = ( the Mult of [:X,Y:] | [:REAL, the carrier of [:X1,Y1:]:]) . z

proof

let z be object ; :: thesis: ( z in dom the Mult of [:X1,Y1:] implies the Mult of [:X1,Y1:] . z = ( the Mult of [:X,Y:] | [:REAL, the carrier of [:X1,Y1:]:]) . z )
assume z in dom the Mult of [:X1,Y1:] ; :: thesis: the Mult of [:X1,Y1:] . z = ( the Mult of [:X,Y:] | [:REAL, the carrier of [:X1,Y1:]:]) . z
then consider x, y being object such that
A16: ( x in REAL & y in the carrier of [:X1,Y1:] & z = [x,y] ) by ZFMISC_1:def 2;
reconsider y = y as Point of [:X1,Y1:] by A16;
reconsider x = x as Element of REAL by A16;
consider az being Point of X1, bz being Point of Y1 such that
A17: y = [az,bz] by PRVECT_3:9;
reconsider az0 = az as Point of X by A1;
reconsider bz0 = bz as Point of Y by A2;
reconsider y1 = [az0,bz0] as Point of [:X,Y:] ;
A18: x * az = x * az0 by RLSUB_1:14;
thus the Mult of [:X1,Y1:] . z = the Mult of [:X1,Y1:] . (x,y) by A16
.= x * y
.= [(x * az),(x * bz)] by PRVECT_3:9, A17
.= [(x * az0),(x * bz0)] by A18, RLSUB_1:14
.= x * y1 by PRVECT_3:9
.= ( the Mult of [:X,Y:] | [:REAL, the carrier of [:X1,Y1:]:]) . [x,y1] by A17, FUNCT_1:49, ZFMISC_1:87
.= ( the Mult of [:X,Y:] | [:REAL, the carrier of [:X1,Y1:]:]) . z by A16, A17 ; :: thesis: verum

end;

then the Mult of [:X1,Y1:] = the Mult of [:X,Y:] | [:REAL, the carrier of [:X1,Y1:]:] by A14, A15, FUNCT_1:2;
hence [:X1,Y1:] is Subspace of [:X,Y:] by A1, A2, A4, A12, RLSUB_1:def 2, ZFMISC_1:96; :: thesis: verum