let y be Element of X1; :: thesis: ( y = x `1_3 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds
y = x1 )
thus ( y = x `1_3 implies for x1, x2, x3 being object st x = [x1,x2,x3] holds
y = x1 ) ; :: thesis: ( ( for x1, x2, x3 being object st x = [x1,x2,x3] holds
y = x1 ) implies y = x `1_3 )
assume A2: for x1, x2, x3 being object st x = [x1,x2,x3] holds
y = x1 ; :: thesis: y = x `1_3
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A3: x = [xx1,xx2,xx3] by Lm2;
thus y = x `1_3 by A2, A3; :: thesis: verum