let T1, T2 be strict OSAlgebra of S; :: thesis: ( the Sorts of T1 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,T1) = (Args (o,T1)) --> z1 ) & the Sorts of T2 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,T2) = (Args (o,T2)) --> z1 ) implies T1 = T2 )
assume that
A5: the Sorts of T1 = ConstOSSet (S,z) and
A6: for o being OperSymbol of S holds Den (o,T1) = (Args (o,T1)) --> z1 ; :: thesis: ( not the Sorts of T2 = ConstOSSet (S,z) or ex o being OperSymbol of S st not Den (o,T2) = (Args (o,T2)) --> z1 or T1 = T2 )
assume that
A7: the Sorts of T2 = ConstOSSet (S,z) and
A8: for o being OperSymbol of S holds Den (o,T2) = (Args (o,T2)) --> z1 ; :: thesis: T1 = T2

now :: thesis: for o1 being object st o1 in the carrier' of S holds
the Charact of T1 . o1 = the Charact of T2 . o1

let o1 be object ; :: thesis: ( o1 in the carrier' of S implies the Charact of T1 . o1 = the Charact of T2 . o1 )
assume o1 in the carrier' of S ; :: thesis: the Charact of T1 . o1 = the Charact of T2 . o1
then reconsider o = o1 as OperSymbol of S ;
thus the Charact of T1 . o1 = Den (o,T1) by MSUALG_1:def 6
.= (Args (o,T1)) --> z1 by A6
.= ((((ConstOSSet (S,z)) #) * the Arity of S) . o) --> z1 by A5, MSUALG_1:def 4
.= (Args (o,T2)) --> z1 by A7, MSUALG_1:def 4
.= Den (o,T2) by A8
.= the Charact of T2 . o1 by MSUALG_1:def 6 ; :: thesis: verum

end;

hence T1 = T2 by A5, A7, PBOOLE:3; :: thesis: verum