let a, b, d be Element of A; :: thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))
A1: ( a = In (0,2) or a = In (1,2) ) by Lm3, Lm4, CARD_1:50, TARSKI:def 2;
A2: ( b = In (0,2) or b = In (1,2) ) by Lm3, Lm4, CARD_1:50, TARSKI:def 2;
A3: ( d = In (0,2) or d = In (1,2) ) by Lm3, Lm4, CARD_1:50, TARSKI:def 2;

per cases ( a = In (0,2) or b = In (0,2) or d = In (0,2) or ( a = In (1,2) & b = In (1,2) & d = In (1,2) ) ) by Lm3, Lm4, CARD_1:50, TARSKI:def 2;

suppose a = In (0,2) ; :: thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))

hence add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d))) by A2, A3, Lm8, Lm9, Lm10, Lm11; :: thesis: verum

end;

suppose b = In (0,2) ; :: thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))

hence add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d))) by A1, A3, Lm8, Lm9, Lm10; :: thesis: verum

end;

suppose d = In (0,2) ; :: thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))

hence add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d))) by A1, A2, Lm8, Lm9, Lm10, Lm11; :: thesis: verum

end;

suppose ( a = In (1,2) & b = In (1,2) & d = In (1,2) ) ; :: thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))

hence add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d))) by Lm9, Lm10, Lm11; :: thesis: verum

end;

end;