for A being non degenerated commutative Ring
for I being Ideal of A
for f, g being FinSequence of bool the carrier of A st len f >= len g & len g > 0 & I ||^ (len f) = f . (len f) & f . 1 = I & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = I *' (f /. i) ) & I ||^ (len g) = g . (len g) & g . 1 = I & ( for i being Nat st i in dom g & i + 1 in dom g holds
g . (i + 1) = I *' (g /. i) ) holds
f | (dom g) = g