let x, y, z be non pair set ; :: thesis: 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: ( not InputVertices (GFA2AdderStr x,y,z) is with_pair & InnerVertices (GFA2AdderStr x,y,z) is Relation ) by FACIRC_1:58, FACIRC_1:59;
A2: ( not InputVertices (GFA2CarryStr x,y,z) is with_pair & InnerVertices (GFA2CarryStr x,y,z) is Relation ) by Th88, Th91;
( InputVertices (GFA2AdderStr x,y,z) = {x,y,z} & InputVertices (GFA2CarryStr x,y,z) = {x,y,z} ) by Th95, FACIRC_1:57;
hence InputVertices (BitGFA2Str x,y,z) = {x,y,z} \/ {x,y,z} by A1, A2, FACIRC_1:7
.= {x,y,z} ;
:: thesis: verum