let E, F, G be 1-sorted ; :: thesis: for x being object st x in [: the carrier of E, the carrier of F, the carrier of G:] holds

ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]

let x be object ; :: thesis: ( x in [: the carrier of E, the carrier of F, the carrier of G:] implies ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3] )

assume x in [: the carrier of E, the carrier of F, the carrier of 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 x1, x2, x3 being object such that

A1: ( x1 in the carrier of E & x2 in the carrier of F & x3 in the carrier of G & x = [x1,x2,x3] ) by MCART_1:68;

reconsider x1 = x1 as Point of E by A1;

reconsider x2 = x2 as Point of F by A1;

reconsider x3 = x3 as Point of G by A1;

take x1 ; :: thesis: ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]

take x2 ; :: thesis: ex x3 being Point of G st x = [x1,x2,x3]

take x3 ; :: thesis: x = [x1,x2,x3]

thus x = [x1,x2,x3] by A1; :: thesis: verum

ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]

let x be object ; :: thesis: ( x in [: the carrier of E, the carrier of F, the carrier of G:] implies ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3] )

assume x in [: the carrier of E, the carrier of F, the carrier of 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 x1, x2, x3 being object such that

A1: ( x1 in the carrier of E & x2 in the carrier of F & x3 in the carrier of G & x = [x1,x2,x3] ) by MCART_1:68;

reconsider x1 = x1 as Point of E by A1;

reconsider x2 = x2 as Point of F by A1;

reconsider x3 = x3 as Point of G by A1;

take x1 ; :: thesis: ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]

take x2 ; :: thesis: ex x3 being Point of G st x = [x1,x2,x3]

take x3 ; :: thesis: x = [x1,x2,x3]

thus x = [x1,x2,x3] by A1; :: thesis: verum