:: deftheorem Def2 defines Fix_inp_ext CIRCUIT2:def 2 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for b₄ being ManySortedFunction of (FreeEnv A),(FreeEnv A) holds
( b₄ = Fix_inp_ext iv iff ( b₄ is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b₄ ) );