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)] ) )

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)] ) )

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

( 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

thus
for x1, y1 being Point of E
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] )

end;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:] )

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: verumassume
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;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

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

thus
0. [:E,F,G:] = [(0. E),(0. F),(0. G)]
; :: thesis: for x1 being Point of E
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;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

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