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

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) <> {}

hence
E is feasible
by MSUALG_6:def 1; :: thesis: verumResult (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;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