let x be pair set ; :: thesis: x = [(x `1),(x `2)]
consider a, b being set such that
A1: x = [a,b] by FACIRC_1:def 1;
( x `1 = a & x `2 = b ) by A1, MCART_1:7;
hence x = [(x `1),(x `2)] by A1; :: thesis: verum