let y4 be set ; :: thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y4 = xx4 ) holds
y4 = x `4_4
let X1, X2, X3, X4 be non empty set ; :: thesis: for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y4 = xx4 ) holds
y4 = x `4_4
let x be Element of [:X1,X2,X3,X4:]; :: thesis: ( ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y4 = xx4 ) implies y4 = x `4_4 )
assume A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y4 = xx4 ; :: thesis: y4 = x `4_4
x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
hence y4 = x `4_4 by A2; :: thesis: verum