set M = the feasible MSAlgebra over S;
take E = MSAlgebra(# the Sorts of the feasible MSAlgebra over S, the Charact of the feasible MSAlgebra over S #); :: thesis: ( E is strict & E is feasible )
thus E is strict ; :: thesis: E is feasible
now :: thesis: for o being OperSymbol of S st Args (o,E) <> {} holds
Result (o,E) <> {}
let o be OperSymbol of S; :: thesis: ( Args (o,E) <> {} implies Result (o,E) <> {} )
A1: Args (o, the feasible MSAlgebra over S) = (( the Sorts of E #) * the Arity of S) . o by MSUALG_1:def 4
.= Args (o,E) by MSUALG_1:def 4 ;
Result (o, the feasible MSAlgebra over S) = ( the Sorts of E * the ResultSort of S) . o by MSUALG_1:def 5
.= Result (o,E) by MSUALG_1:def 5 ;
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