let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being MSAlgebra over S st U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 holds

MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

let U1, U2 be MSAlgebra over S; :: thesis: ( U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )

assume that

A1: U1 is MSSubAlgebra of U2 and

A2: U2 is MSSubAlgebra of U1 ; :: thesis: MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

the Sorts of U2 is MSSubset of U1 by A2, Def9;

then A3: the Sorts of U2 c= the Sorts of U1 by PBOOLE:def 18;

reconsider B1 = the Sorts of U1 as MSSubset of U2 by A1, Def9;

A4: the Charact of U1 = Opers (U2,B1) by A1, Def9;

reconsider B2 = the Sorts of U2 as MSSubset of U1 by A2, Def9;

A5: the Charact of U2 = Opers (U1,B2) by A2, Def9;

the Sorts of U1 is MSSubset of U2 by A1, Def9;

then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def 18;

then A6: the Sorts of U1 = the Sorts of U2 by A3, PBOOLE:146;

set O = the Charact of U1;

set P = Opers (U1,B2);

A7: B1 is opers_closed by A1, Def9;

for x being object st x in the carrier' of S holds

the Charact of U1 . x = (Opers (U1,B2)) . x

MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

let U1, U2 be MSAlgebra over S; :: thesis: ( U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )

assume that

A1: U1 is MSSubAlgebra of U2 and

A2: U2 is MSSubAlgebra of U1 ; :: thesis: MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

the Sorts of U2 is MSSubset of U1 by A2, Def9;

then A3: the Sorts of U2 c= the Sorts of U1 by PBOOLE:def 18;

reconsider B1 = the Sorts of U1 as MSSubset of U2 by A1, Def9;

A4: the Charact of U1 = Opers (U2,B1) by A1, Def9;

reconsider B2 = the Sorts of U2 as MSSubset of U1 by A2, Def9;

A5: the Charact of U2 = Opers (U1,B2) by A2, Def9;

the Sorts of U1 is MSSubset of U2 by A1, Def9;

then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def 18;

then A6: the Sorts of U1 = the Sorts of U2 by A3, PBOOLE:146;

set O = the Charact of U1;

set P = Opers (U1,B2);

A7: B1 is opers_closed by A1, Def9;

for x being object st x in the carrier' of S holds

the Charact of U1 . x = (Opers (U1,B2)) . x

proof

hence
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
by A6, A5, PBOOLE:3; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier' of S implies the Charact of U1 . x = (Opers (U1,B2)) . x )

assume x in the carrier' of S ; :: thesis: the Charact of U1 . x = (Opers (U1,B2)) . x

then reconsider o = x as OperSymbol of S ;

A8: Args (o,U2) = ((B2 #) * the Arity of S) . o by MSUALG_1:def 4;

A9: B1 is_closed_on o by A7;

thus the Charact of U1 . x = o /. B1 by A4, Def8

.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A9, Def7

.= Den (o,U2) by A6, A8

.= (Opers (U1,B2)) . x by A5, MSUALG_1:def 6 ; :: thesis: verum

end;assume x in the carrier' of S ; :: thesis: the Charact of U1 . x = (Opers (U1,B2)) . x

then reconsider o = x as OperSymbol of S ;

A8: Args (o,U2) = ((B2 #) * the Arity of S) . o by MSUALG_1:def 4;

A9: B1 is_closed_on o by A7;

thus the Charact of U1 . x = o /. B1 by A4, Def8

.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A9, Def7

.= Den (o,U2) by A6, A8

.= (Opers (U1,B2)) . x by A5, MSUALG_1:def 6 ; :: thesis: verum