let T1, T2 be strict OSAlgebra of S; ( 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
; ( 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
; T1 = T2
hence
T1 = T2
by A5, A7, PBOOLE:3; verum