let y be Element of X1; :: thesis: ( y = x `1_4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1 )
thus ( y = x `1_4 implies for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1 ) :: thesis: ( ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1 ) implies y = x `1_4 )

proof

assume Z: y = x `1_4 ; :: thesis: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1
let x1, x2, x3, x4 be set ; :: thesis: ( x = [x1,x2,x3,x4] implies y = x1 )
assume W: x = [x1,x2,x3,x4] ; :: thesis: y = x1
[x1,x2,x3,x4] `1_4 = x1 ;
hence y = x1 by W, Z; :: thesis: verum

end;

assume Z: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1 ; :: thesis: y = x `1_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;
[xx1,xx2,xx3,xx4] `1_4 = xx1 ;
hence y = x `1_4 by Z, A6; :: thesis: verum