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 Lm2, CARD_1:88, TARSKI:def 2;
A2: ( b = In 0 ,2 or b = In 1,2 ) by Lm2, CARD_1:88, TARSKI:def 2;
A3: ( d = In 0 ,2 or d = In 1,2 ) by Lm2, CARD_1:88, 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 Lm2, CARD_1:88, 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, Lm6, Lm7, Lm8, Lm9; :: 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, Lm6, Lm7, Lm8; :: 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, Lm6, Lm7, Lm8, Lm9; :: 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 Lm7, Lm8, Lm9; :: thesis: verum

end;

end;