let f1 be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: for x, y, z, a, b being set holds GFA0CarryOutput (x,y,z) <> [<*a,b*>,f1]
let x, y, z be set ; :: thesis: for a, b being set holds GFA0CarryOutput (x,y,z) <> [<*a,b*>,f1]
let a, b be set ; :: thesis: GFA0CarryOutput (x,y,z) <> [<*a,b*>,f1]
set xy = [<*x,y*>,and2];
set yz = [<*y,z*>,and2];
set zx = [<*z,x*>,and2];
set A1 = GFA0CarryOutput (x,y,z);
A1: (GFA0CarryOutput (x,y,z)) `1 = <*[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]*> ;
( len <*[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]*> = 3 & len <*a,b*> = 2 ) by FINSEQ_1:44, FINSEQ_1:45;
hence GFA0CarryOutput (x,y,z) <> [<*a,b*>,f1] by A1; :: thesis: verum