let X1, X2, X3, y2 be set ; :: thesis: for x being Element of [:X1,X2,X3:] st X1 <> {} & X2 <> {} & X3 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y2 = xx2 ) holds
y2 = x `2
let x be Element of [:X1,X2,X3:]; :: thesis: ( X1 <> {} & X2 <> {} & X3 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y2 = xx2 ) implies y2 = x `2 )
assume that
A1: ( X1 <> {} & X2 <> {} & X3 <> {} ) and
A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y2 = xx2 ; :: thesis: y2 = x `2
x = [(x `1),(x `2),(x `3)] by A1, Th48;
hence y2 = x `2 by A2; :: thesis: verum