theorem Th19: :: GFACIRC2:19

for n being Nat
for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitGFA1Str ((p ^ p1),(q ^ q1)) = n -BitGFA1Str ((p ^ p2),(q ^ q2)) & n -BitGFA1Circ ((p ^ p1),(q ^ q1)) = n -BitGFA1Circ ((p ^ p2),(q ^ q2)) & n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) )