let x, y, z be non pair set ; InputVertices (BitGFA2Str (x,y,z)) = {x,y,z}
set S = BitGFA2Str (x,y,z);
set S1 = GFA2AdderStr (x,y,z);
set S2 = GFA2CarryStr (x,y,z);
A1:
( InputVertices (GFA2AdderStr (x,y,z)) = {x,y,z} & InputVertices (GFA2CarryStr (x,y,z)) = {x,y,z} )
by Th82, FACIRC_1:57;
( InnerVertices (GFA2AdderStr (x,y,z)) is Relation & InnerVertices (GFA2CarryStr (x,y,z)) is Relation )
by Th75, FACIRC_1:58;
hence InputVertices (BitGFA2Str (x,y,z)) =
{x,y,z} \/ {x,y,z}
by A1, FACIRC_1:7
.=
{x,y,z}
;
verum