let S be non void Signature; :: thesis: for A being feasible MSAlgebra over S
for B being MSSubAlgebra of A holds B is feasible
let A be feasible MSAlgebra over 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 9;
let o be OperSymbol of S; :: according to MSUALG_6:def 1 :: thesis: ( Args (o,B) = {} or not Result (o,B) = {} )
set a = the Element of Args (o,B);
assume Args (o,B) <> {} ; :: thesis: not Result (o,B) = {}
then A1: the Element of Args (o,B) in Args (o,B) ;
A2: Args (o,B) c= Args (o,A) by Th37;
then Result (o,A) <> {} by A1, MSUALG_6:def 1;
then dom (Den (o,A)) = Args (o,A) by FUNCT_2:def 1;
then the Element of Args (o,B) in dom ((Den (o,A)) | (Args (o,B))) by A1, A2, RELAT_1:57;
then A3: ( Result (o,B) = (SB * the ResultSort of S) . o & ((Den (o,A)) | (Args (o,B))) . the Element of Args (o,B) in rng ((Den (o,A)) | (Args (o,B))) ) by FUNCT_1:def 3, MSUALG_1:def 5;
SB is opers_closed by MSUALG_2:def 9;
then SB is_closed_on o ;
then rng ((Den (o,A)) | (((SB #) * the Arity of S) . o)) c= (SB * the ResultSort of S) . o ;
hence not Result (o,B) = {} by A3, MSUALG_1:def 4; :: thesis: verum