let U1, U2 be Universal_Algebra; ( 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
; 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); ( B = the Sorts of (MSAlg U1) implies B is opers_closed )
assume A2:
B = the Sorts of (MSAlg U1)
; B is opers_closed
let o be OperSymbol of (MSSign U2); MSUALG_2:def 6 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; verum