consider C being image of A such that
A1: C is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S by Def14;
thus ex b₁ being bool-correct image of A st
( b₁ is 4,1 integer & b₁ is 11,1,1 -array ) by A1; :: thesis: verum