let G, F be non empty RLSStruct ; :: thesis: ( ( for x being set holds
( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]
for x1, y1 being Point of G
for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) )
for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]

proof

let x be Point of [:G,F:]; :: thesis: for x1 being Point of G
for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
let x1 be Point of G; :: thesis: for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
let x2 be Point of F; :: thesis: for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
let a be real number ; :: thesis: ( x = [x1,x2] implies a * x = [(a * x1),(a * x2)] )
reconsider a0 = a as Element of REAL by XREAL_0:def 1;
assume A1: x = [x1,x2] ; :: thesis: a * x = [(a * x1),(a * x2)]
a * x = (prod_MLT (G,F)) . (a0,x) ;
hence a * x = [(a * x1),(a * x2)] by A1, Def2; :: thesis: verum

end;

hence ( ( for x being set holds
( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]
for x1, y1 being Point of G
for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) ) by Def1, Lm1; :: thesis: verum