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 6 :: 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 5;
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 4, 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; :: thesis: verum