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

let o1 be set ; :: 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 11
.= (Args o,T1) --> z1 by A6
.= ((((ConstOSSet S,z) # ) * the Arity of S) . o) --> z1 by A5, MSUALG_1:def 9
.= (Args o,T2) --> z1 by A7, MSUALG_1:def 9
.= Den o,T2 by A8
.= the Charact of T2 . o1 by MSUALG_1:def 11 ; :: thesis: verum

end;

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