let y be Element of X2; :: thesis: ( y = x `2_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
y = x2 )
thus ( y = x `2_4 implies for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
y = x2 ) ; :: thesis: ( ( for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
y = x2 ) implies y = x `2_4 )
assume A5: for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
y = x2 ; :: thesis: y = x `2_4
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
thus y = x `2_4 by A5, A6; :: thesis: verum