consider M being feasible MSAlgebra of S;
take E = MSAlgebra(# the Sorts of M,the Charact of M #); :: thesis: ( E is strict & E is feasible )
thus E is strict ; :: thesis: E is feasible

now

let o be OperSymbol of S; :: thesis: ( Args o,E <> {} implies Result o,E <> {} )
A1: Result o,M = (the Sorts of E * the ResultSort of S) . o by MSUALG_1:def 10
.= Result o,E by MSUALG_1:def 10 ;
Args o,M = ((the Sorts of E # ) * the Arity of S) . o by MSUALG_1:def 9
.= Args o,E by MSUALG_1:def 9 ;
hence ( Args o,E <> {} implies Result o,E <> {} ) by A1, MSUALG_6:def 1; :: thesis: verum

end;

hence E is feasible by MSUALG_6:def 1; :: thesis: verum