let MS be non void 1 -element segmental ManySortedSign ; :: thesis: for A, B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
let A, B be non-empty MSAlgebra over MS; :: thesis: ( 1-Alg A = 1-Alg B implies MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) )
assume A1: 1-Alg A = 1-Alg B ; :: thesis: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
A2: 1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def 14;
A3: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def 14;
A4: now :: thesis: for i being object st i in the carrier of MS holds
the Sorts of A . i = the Sorts of B . i
let i be object ; :: thesis: ( i in the carrier of MS implies the Sorts of A . i = the Sorts of B . i )
assume A5: i in the carrier of MS ; :: thesis: the Sorts of A . i = the Sorts of B . i
A6: ex c being Component of the Sorts of B st the Sorts of B . i = c
proof
reconsider c = the Sorts of B . i as Component of the Sorts of B by A5, PBOOLE:139;
take c ; :: thesis: the Sorts of B . i = c
thus the Sorts of B . i = c ; :: thesis: verum
end;
ex c being Component of the Sorts of A st the Sorts of A . i = c
proof
reconsider c = the Sorts of A . i as Component of the Sorts of A by A5, PBOOLE:139;
take c ; :: thesis: the Sorts of A . i = c
thus the Sorts of A . i = c ; :: thesis: verum
end;
then the Sorts of A . i = the_sort_of B by A1, A3, A2, MSUALG_1:def 12
.= the Sorts of B . i by A6, MSUALG_1:def 12 ;
hence the Sorts of A . i = the Sorts of B . i ; :: thesis: verum
end;
the Charact of A = the charact of (1-Alg A) by A3, MSUALG_1:def 13
.= the Charact of B by A1, A2, MSUALG_1:def 13 ;
hence MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) by A4, PBOOLE:3; :: thesis: verum