( [0 ,0 ] `2 = 0 & [0 ,1] `2 = 1 & [0 ,2] `2 = 2 & [0 ,3] `2 = 3 & [0 ,4] `2 = 4 ) by MCART_1:7;
hence for b₁ being Integer holds
( ( o = [0 ,0 ] & o = [0 ,1] implies ( b₁ = i + j iff b₁ = i - j ) ) & ( o = [0 ,0 ] & o = [0 ,2] implies ( b₁ = i + j iff b₁ = i * j ) ) & ( o = [0 ,0 ] & o = [0 ,3] implies ( b₁ = i + j iff b₁ = i div j ) ) & ( o = [0 ,0 ] & o = [0 ,4] implies ( b₁ = i + j iff b₁ = i mod j ) ) & ( o = [0 ,1] & o = [0 ,2] implies ( b₁ = i - j iff b₁ = i * j ) ) & ( o = [0 ,1] & o = [0 ,3] implies ( b₁ = i - j iff b₁ = i div j ) ) & ( o = [0 ,1] & o = [0 ,4] implies ( b₁ = i - j iff b₁ = i mod j ) ) & ( o = [0 ,2] & o = [0 ,3] implies ( b₁ = i * j iff b₁ = i div j ) ) & ( o = [0 ,2] & o = [0 ,4] implies ( b₁ = i * j iff b₁ = i mod j ) ) & ( o = [0 ,3] & o = [0 ,4] implies ( b₁ = i div j iff b₁ = i mod j ) ) ) ; :: thesis: verum