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 x = [[a1,a2],[b1,b2]] ; :: thesis: ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 )
then ( x `1 = [a1,a2] & x `2 = [b1,b2] ) by MCART_1:7;
hence ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 ) by MCART_1:7; :: thesis: verum