let U be Universe; :: thesis: for x being Element of U
for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U )
let x be Element of U; :: thesis: for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U )
let x1, x2, x3, x4 be object ; :: thesis: ( x = [x1,x2,x3,x4] implies ( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U ) )
assume x = [x1,x2,x3,x4] ; :: thesis: ( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U )
then x = [[x1,x2,x3],x4] by XTUPLE_0:def 8;
then ( x4 is Element of U & [x1,x2,x3] is Element of U ) by CLASSES4:22;
hence ( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U ) by Th11; :: thesis: verum