let S be non void Signature; :: thesis: for A being feasible MSAlgebra of S
for B being MSSubAlgebra of A holds B is feasible
let A be feasible MSAlgebra of S; :: thesis: for B being MSSubAlgebra of A holds B is feasible
let B be MSSubAlgebra of A; :: thesis: B is feasible
reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def 10;
let o be OperSymbol of S; :: according to MSUALG_6:def 1 :: thesis: ( Args (o,B) = {} or not Result (o,B) = {} )
consider a being Element of Args (o,B);
assume Args (o,B) <> {} ; :: thesis: not Result (o,B) = {}
then A1: a in Args (o,B) ;
A2: Args (o,B) c= Args (o,A) by Th38;
then Result (o,A) <> {} by A1, MSUALG_6:def 1;
then dom (Den (o,A)) = Args (o,A) by FUNCT_2:def 1;
then a in dom ((Den (o,A)) | (Args (o,B))) by A1, A2, RELAT_1:86;
then A3: ( Result (o,B) = (SB * the ResultSort of S) . o & ((Den (o,A)) | (Args (o,B))) . a in rng ((Den (o,A)) | (Args (o,B))) ) by FUNCT_1:def 5, MSUALG_1:def 10;
SB is opers_closed by MSUALG_2:def 10;
then SB is_closed_on o by MSUALG_2:def 7;
then rng ((Den (o,A)) | (((SB #) * the Arity of S) . o)) c= (SB * the ResultSort of S) . o by MSUALG_2:def 6;
hence not Result (o,B) = {} by A3, MSUALG_1:def 9; :: thesis: verum