let x, y, z be set ; :: thesis: for p being set holds GFA2AdderOutput x,y,z <> [p,and2a ]
let p be set ; :: thesis: GFA2AdderOutput x,y,z <> [p,and2a ]
set A1 = GFA2AdderOutput x,y,z;

now

assume [p,and2a ] `2 = (GFA2AdderOutput x,y,z) `2 ; :: thesis: contradiction
then A1: [p,and2a ] `2 = xor2c by MCART_1:7;
[p,and2a ] `2 = and2a by MCART_1:7;
hence contradiction by A1, GFACIRC1:4, TWOSCOMP:11; :: thesis: verum

end;

hence GFA2AdderOutput x,y,z <> [p,and2a ] ; :: thesis: verum