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
A3: MSSign U1 = MSSign U2 by A1, Th7;
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;
A4: rng (Den a,(MSAlg U1)) c= Result a,(MSAlg U1) by RELAT_1:def 19;
set Z = rng ((Den o,(MSAlg U2)) | (((B # ) * the Arity of (MSSign U2)) . a));
A5: rng ((Den o,(MSAlg U2)) | (((B # ) * the Arity of (MSSign U2)) . a)) = rng ((Den o,(MSAlg U2)) | (Args a,(MSAlg U1))) by A2, A3, MSUALG_1:def 9;
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 A6: (B * the ResultSort of (MSSign U2)) . a = Result a,(MSAlg U1) by MSUALG_1:def 10;
rng ((Den o,(MSAlg U2)) | (((B # ) * the Arity of (MSSign U2)) . a)) c= Result a,(MSAlg U1) by A1, A2, A4, A5, Th8;
hence B is_closed_on o by A6, MSUALG_2:def 6; :: thesis: verum