let d be set ; :: thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( d = x `4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 )
let X1, X2, X3, X4 be non empty set ; :: thesis: for x being Element of [:X1,X2,X3,X4:] holds
( d = x `4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 )
let x be Element of [:X1,X2,X3,X4:]; :: thesis: ( d = x `4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 )
thus ( d = x `4 implies for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 ) :: thesis: ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 ) implies d = x `4 )

proof

assume A1: d = x `4 ; :: thesis: for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4
let x1 be Element of X1; :: thesis: for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4
let x2 be Element of X2; :: thesis: for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4
let x3 be Element of X3; :: thesis: for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4
let x4 be Element of X4; :: thesis: ( x = [x1,x2,x3,x4] implies d = x4 )
assume A2: x = [x1,x2,x3,x4] ; :: thesis: d = x4
x = [(x `1 ),(x `2 ),(x `3 ),(x `4 )] by MCART_1:60;
hence d = x4 by A1, A2, MCART_1:33; :: thesis: verum

end;

thus ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 ) implies d = x `4 ) by MCART_1:82; :: thesis: verum