( dom A = dom A & ( for i being Element of NAT st i in dom A holds
A . i c= A . i ) ) ;
hence ex b₁ being FinSequence of bool F st
( dom b₁ = dom A & ( for i being Element of NAT st i in dom A holds
b₁ . i c= A . i ) ) ; :: thesis: verum