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: 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 ;
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 ;
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