consider A being Circuit of S such that
A1: ( the Sorts of A is constant & the_value_of the Sorts of A = X ) and
A2: A is gate`2=den by Def9;
set B = MSAlgebra(# the Sorts of A, the Charact of A #);
the Sorts of A is V39() 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 A2;
then B is gate`2=den ;
then reconsider B = B as Circuit of X,S by A1, Def10;
take B ; :: thesis: B is strict
thus B is strict ; :: thesis: verum