let U1, U2 be Universal_Algebra; :: thesis: ( U1 is SubAlgebra of U2 implies for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
B is opers_closed )
assume A1: U1 is SubAlgebra of U2 ; :: thesis: for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
B is opers_closed
let B be MSSubset of (MSAlg U2); :: thesis: ( B = the Sorts of (MSAlg U1) implies B is opers_closed )
assume A2: B = the Sorts of (MSAlg U1) ; :: thesis: B is opers_closed
let o be OperSymbol of (MSSign U2); :: according to MSUALG_2:def 7 :: thesis: B is_closed_on o
reconsider a = o as Element of the carrier' of (MSSign U1) by A1, Th7;
set S = (B * the ResultSort of (MSSign U2)) . a;
(B * the ResultSort of (MSSign U2)) . a = (the Sorts of (MSAlg U1) * the ResultSort of (MSSign U1)) . a by A1, A2, Th7;
then A3: (B * the ResultSort of (MSSign U2)) . a = Result a,(MSAlg U1) by MSUALG_1:def 10;
set Z = rng ((Den o,(MSAlg U2)) | (((B # ) * the Arity of (MSSign U2)) . a));
MSSign U1 = MSSign U2 by A1, Th7;
then ( rng (Den a,(MSAlg U1)) c= Result a,(MSAlg U1) & rng ((Den o,(MSAlg U2)) | (((B # ) * the Arity of (MSSign U2)) . a)) = rng ((Den o,(MSAlg U2)) | (Args a,(MSAlg U1))) ) by A2, MSUALG_1:def 9, RELAT_1:def 19;
then rng ((Den o,(MSAlg U2)) | (((B # ) * the Arity of (MSSign U2)) . a)) c= Result a,(MSAlg U1) by A1, A2, Th8;
hence B is_closed_on o by A3, MSUALG_2:def 6; :: thesis: verum