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

thus for x being set holds
( x is Point of [:E,F,G:] iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3] ) :: thesis: ( ( for x1, y1 being Point of E
for x2, y2 being Point of F
for x3, y3 being Point of G holds [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] ) & 0. [:E,F,G:] = [(0. E),(0. F),(0. G)] & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G
for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)] ) )
proof
let x be set ; :: thesis: ( x is Point of [:E,F,G:] iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3] )
hereby :: thesis: ( ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3] implies x is Point of [:E,F,G:] )
assume x is Point of [:E,F,G:] ; :: thesis: ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]
then consider x1x2 being Point of [:E,F:], x3 being Point of G such that
A1: x = [x1x2,x3] by PRVECT_3:9;
consider x1 being Point of E, x2 being Point of F such that
A2: x1x2 = [x1,x2] by PRVECT_3:9;
take x1 = x1; :: thesis: ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]
take x2 = x2; :: thesis: ex x3 being Point of G st x = [x1,x2,x3]
take x3 = x3; :: thesis: x = [x1,x2,x3]
thus x = [x1,x2,x3] by A1, A2; :: thesis: verum
end;
thus ( ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3] implies x is Point of [:E,F,G:] ) ; :: thesis: verum
end;
thus for x1, y1 being Point of E
for x2, y2 being Point of F
for x3, y3 being Point of G holds [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] :: thesis: ( 0. [:E,F,G:] = [(0. E),(0. F),(0. G)] & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G
for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)] ) )
proof
let x1, y1 be Point of E; :: thesis: for x2, y2 being Point of F
for x3, y3 being Point of G holds [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)]

let x2, y2 be Point of F; :: thesis: for x3, y3 being Point of G holds [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)]
let x3, y3 be Point of G; :: thesis: [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)]
[x1,x2] + [y1,y2] = [(x1 + y1),(x2 + y2)] by PRVECT_3:9;
hence [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] by PRVECT_3:9; :: thesis: verum
end;
thus 0. [:E,F,G:] = [(0. E),(0. F),(0. G)] ; :: thesis: for x1 being Point of E
for x2 being Point of F
for x3 being Point of G
for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)]

let x1 be Point of E; :: thesis: for x2 being Point of F
for x3 being Point of G
for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)]

let x2 be Point of F; :: thesis: for x3 being Point of G
for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)]

let x3 be Point of G; :: thesis: for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)]
let a be Real; :: thesis: a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)]
thus a * [x1,x2,x3] = [(a * [x1,x2]),(a * x3)] by PRVECT_3:9
.= [(a * x1),(a * x2),(a * x3)] by PRVECT_3:9 ; :: thesis: verum