let X1, X2, X3, X4, X5 be set ; :: thesis: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} implies for x being Element of [:X1,X2,X3,X4,X5:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] )
assume that
A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) and
A2: X5 <> {} ; :: thesis: for x being Element of [:X1,X2,X3,X4,X5:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5]
let x be Element of [:X1,X2,X3,X4,X5:]; :: thesis: ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5]
reconsider x9 = x as Element of [:[:X1,X2,X3,X4:],X5:] ;
[:X1,X2,X3,X4:] <> {} by A1, MCART_1:51;
then consider x1234 being Element of [:X1,X2,X3,X4:], xx5 being Element of X5 such that
A3: x9 = [x1234,xx5] by A2, Lm1;
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A4: x1234 = [xx1,xx2,xx3,xx4] by A1, Lm3;
take xx1 ; :: thesis: ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5]
take xx2 ; :: thesis: ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5]
take xx3 ; :: thesis: ex xx4 being Element of X4 ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5]
take xx4 ; :: thesis: ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5]
take xx5 ; :: thesis: x = [xx1,xx2,xx3,xx4,xx5]
thus x = [xx1,xx2,xx3,xx4,xx5] by A3, A4; :: thesis: verum