let U be Universe; :: thesis: for x being Element of U
for x1, x2, x3, x4, x5 being object st x = [x1,x2,x3,x4,x5] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U & x5 is Element of U )
let x be Element of U; :: thesis: for x1, x2, x3, x4, x5 being object st x = [x1,x2,x3,x4,x5] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U & x5 is Element of U )
let x1, x2, x3, x4, x5 be object ; :: thesis: ( x = [x1,x2,x3,x4,x5] implies ( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U & x5 is Element of U ) )
assume x = [x1,x2,x3,x4,x5] ; :: thesis: ( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U & x5 is Element of U )
then ( x5 is Element of U & [x1,x2,x3,x4] 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 & x5 is Element of U ) by Th12; :: thesis: verum