let S be non empty non void ManySortedSign ; :: thesis: for A, B being MSAlgebra over S holds
( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )
let A, B be MSAlgebra over S; :: thesis: ( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )
thus ( A is MSSubAlgebra of B implies A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) ) :: thesis: ( A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) implies A is MSSubAlgebra of B )

proof

assume A1: A is MSSubAlgebra of B ; :: thesis: A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #)
hence the Sorts of A is MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) by MSUALG_2:def 9; :: according to MSUALG_2:def 9 :: thesis: for b₁ being ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of B, the Charact of B #) holds
( not b₁ = the Sorts of A or ( b₁ is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),b₁) ) )
thus for BB being MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) st BB = the Sorts of A holds
( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) :: thesis: verum

proof

let BB be MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #); :: thesis: ( BB = the Sorts of A implies ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) )
assume A2: BB = the Sorts of A ; :: thesis: ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) )
reconsider bb = BB as MSSubset of B ;
A3: bb is opers_closed by A1, A2, MSUALG_2:def 9;
A4: BB is opers_closed

proof

let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: BB is_closed_on o
A5: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def 6
.= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def 6 ;
bb is_closed_on o by A3;
then rng ((Den (o,MSAlgebra(# the Sorts of B, the Charact of B #))) | (((BB #) * the Arity of S) . o)) c= (BB * the ResultSort of S) . o by A5;
hence BB is_closed_on o ; :: thesis: verum

end;

for o being object st o in the carrier' of S holds
the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o

proof

let o be object ; :: thesis: ( o in the carrier' of S implies the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o )
assume o in the carrier' of S ; :: thesis: the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o
then reconsider o = o as OperSymbol of S ;
A6: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def 6
.= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def 6 ;
A7: bb is_closed_on o by A3;
A8: BB is_closed_on o by A4;
(Opers (B,bb)) . o = o /. bb by MSUALG_2:def 8
.= (Den (o,MSAlgebra(# the Sorts of B, the Charact of B #))) | (((BB #) * the Arity of S) . o) by A6, A7, MSUALG_2:def 7
.= o /. BB by A8, MSUALG_2:def 7
.= (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o by MSUALG_2:def 8 ;
hence the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o by A1, A2, MSUALG_2:def 9; :: thesis: verum

end;

hence ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) by A4; :: thesis: verum

end;

end;

assume A9: A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) ; :: thesis: A is MSSubAlgebra of B
hence the Sorts of A is MSSubset of B by MSUALG_2:def 9; :: according to MSUALG_2:def 9 :: thesis: for b₁ being ManySortedSubset of the Sorts of B holds
( not b₁ = the Sorts of A or ( b₁ is opers_closed & the Charact of A = Opers (B,b₁) ) )
let C be MSSubset of B; :: thesis: ( not C = the Sorts of A or ( C is opers_closed & the Charact of A = Opers (B,C) ) )
assume A10: C = the Sorts of A ; :: thesis: ( C is opers_closed & the Charact of A = Opers (B,C) )
reconsider CC = C as MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) ;
A11: CC is opers_closed by A9, A10, MSUALG_2:def 9;
A12: C is opers_closed

proof

let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: C is_closed_on o
A13: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def 6
.= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def 6 ;
CC is_closed_on o by A11;
then rng ((Den (o,B)) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o by A13;
hence C is_closed_on o ; :: thesis: verum

end;

for o being object st o in the carrier' of S holds
the Charact of A . o = (Opers (B,C)) . o

proof

let o be object ; :: thesis: ( o in the carrier' of S implies the Charact of A . o = (Opers (B,C)) . o )
assume o in the carrier' of S ; :: thesis: the Charact of A . o = (Opers (B,C)) . o
then reconsider o = o as OperSymbol of S ;
A14: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def 6
.= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def 6 ;
A15: CC is_closed_on o by A11;
A16: C is_closed_on o by A12;
(Opers (MSAlgebra(# the Sorts of B, the Charact of B #),CC)) . o = o /. CC by MSUALG_2:def 8
.= (Den (o,B)) | (((C #) * the Arity of S) . o) by A14, A15, MSUALG_2:def 7
.= o /. C by A16, MSUALG_2:def 7
.= (Opers (B,C)) . o by MSUALG_2:def 8 ;
hence the Charact of A . o = (Opers (B,C)) . o by A9, A10, MSUALG_2:def 9; :: thesis: verum

end;

hence ( C is opers_closed & the Charact of A = Opers (B,C) ) by A12; :: thesis: verum