A1: ( [0,2] `2 = 2 & [0,3] `2 = 3 ) by MCART_1:7;
( [0,0] `2 = 0 & [0,1] `2 = 1 ) 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 ) ) ) by A1, MCART_1:7; :: thesis: verum