let x, a1, a2, b1, b2 be set ; :: thesis: ( x = [[a1,a2],[b1,b2]] implies ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 ) )
assume A1: x = [[a1,a2],[b1,b2]] ; :: thesis: ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 )
then A2: x `1 = [a1,a2] by MCART_1:7;
x `2 = [b1,b2] by A1, MCART_1:7;
hence ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 ) by A2, MCART_1:7; :: thesis: verum