let a be set ; for X1, X2, X3, X4 being non empty set holds
( a in [:X1,X2,X3,X4:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] )
let X1, X2, X3, X4 be non empty set ; ( a in [:X1,X2,X3,X4:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] )
thus
( a in [:X1,X2,X3,X4:] implies ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] )
( ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] implies a in [:X1,X2,X3,X4:] )proof
assume
a in [:X1,X2,X3,X4:]
;
ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4]
then
a in [:[:X1,X2,X3:],X4:]
by ZFMISC_1:def 4;
then consider x123,
x4 being
object such that A1:
x123 in [:X1,X2,X3:]
and A2:
x4 in X4
and A3:
a = [x123,x4]
by ZFMISC_1:def 2;
reconsider x4 =
x4 as
Element of
X4 by A2;
consider x1 being
Element of
X1,
x2 being
Element of
X2,
x3 being
Element of
X3 such that A4:
x123 = [x1,x2,x3]
by A1, Th3;
a = [x1,x2,x3,x4]
by A3, A4;
hence
ex
x1 being
Element of
X1 ex
x2 being
Element of
X2 ex
x3 being
Element of
X3 ex
x4 being
Element of
X4 st
a = [x1,x2,x3,x4]
;
verum
end;
given x1 being Element of X1, x2 being Element of X2, x3 being Element of X3, x4 being Element of X4 such that A5:
a = [x1,x2,x3,x4]
; a in [:X1,X2,X3,X4:]
a = [[x1,x2,x3],x4]
by A5;
then
a in [:[:X1,X2,X3:],X4:]
;
hence
a in [:X1,X2,X3,X4:]
by ZFMISC_1:def 4; verum