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