let E, F, G be non empty addLoopStr ; :: 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)] )

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

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

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

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

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

consider x1 being Point of E, x2 being Point of F such that

A2: x1x2 = [x1,x2] by PRVECT_3:7;

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

consider x1 being Point of E, x2 being Point of F such that

A2: x1x2 = [x1,x2] by PRVECT_3:7;

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

hereby :: thesis: 0. [:E,F,G:] = [(0. E),(0. F),(0. G)]

thus
0. [:E,F,G:] = [(0. E),(0. F),(0. G)]
; :: thesis: verumlet 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:7;

hence [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] by PRVECT_3:7; :: 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:7;

hence [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] by PRVECT_3:7; :: thesis: verum