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