let X1, X2, X3 be set ; ( X1 <> {} & X2 <> {} & X3 <> {} implies for x being Element of [:X1,X2,X3:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3] )
assume that
A1:
( X1 <> {} & X2 <> {} )
and
A2:
X3 <> {}
; for x being Element of [:X1,X2,X3:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3]
let x be Element of [:X1,X2,X3:]; ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3]
reconsider x9 = x as Element of [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
consider x12 being Element of [:X1,X2:], xx3 being Element of X3 such that
A3:
x9 = [x12,xx3]
by A1, A2, Lm1;
consider xx1 being Element of X1, xx2 being Element of X2 such that
A4:
x12 = [xx1,xx2]
by A1, Lm1;
take
xx1
; ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3]
take
xx2
; ex xx3 being Element of X3 st x = [xx1,xx2,xx3]
take
xx3
; x = [xx1,xx2,xx3]
thus
x = [xx1,xx2,xx3]
by A3, A4; verum