consider A being Circuit of S such that
A1: ( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den ) by Def9;
set B = MSAlgebra(# the Sorts of A,the Charact of A #);
the Sorts of A is finite-yielding by MSAFREE2:def 11;
then reconsider B = MSAlgebra(# the Sorts of A,the Charact of A #) as Circuit of S by MSAFREE2:def 11;
for g being set st g in the carrier' of S holds
g = [(g `1 ),(the Charact of B . g)] by A1, CIRCCOMB:def 10;
then ( B is gate`2=den & the Sorts of B is constant & the_value_of the Sorts of B = X ) by A1, CIRCCOMB:def 10;
then reconsider B = B as Circuit of X,S by Def10;
take B ; :: thesis: B is strict
thus B is strict ; :: thesis: verum