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

proof

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

end;

thus ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 ) implies c = x `3 ) by MCART_1:71; :: thesis: verum