let y3 be object ; :: thesis: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y3 = xx3 ) holds
y3 = x `3_3
let X1, X2, X3 be non empty set ; :: thesis: for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y3 = xx3 ) holds
y3 = x `3_3
let x be Element of [:X1,X2,X3:]; :: thesis: ( ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y3 = xx3 ) implies y3 = x `3_3 )
assume A1: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y3 = xx3 ; :: thesis: y3 = x `3_3
x = [(x `1_3),(x `2_3),(x `3_3)] ;
hence y3 = x `3_3 by A1; :: thesis: verum