let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for o being OperSymbol of S st the Arity of S . o = {} holds
dom (Den o,A) = {{} }
let A be non-empty MSAlgebra of S; :: thesis: for o being OperSymbol of S st the Arity of S . o = {} holds
dom (Den o,A) = {{} }
let o be OperSymbol of S; :: thesis: ( the Arity of S . o = {} implies dom (Den o,A) = {{} } )
assume A1:
the Arity of S . o = {}
; :: thesis: dom (Den o,A) = {{} }
A2:
dom (the Sorts of A # ) = the carrier of S *
by PARTFUN1:def 4;
A3:
( dom the Arity of S = the carrier' of S & rng the Arity of S c= the carrier of S * )
by FUNCT_2:def 1, RELAT_1:def 19;
then
the Arity of S . o in rng the Arity of S
by FUNCT_1:def 5;
then A4:
o in dom ((the Sorts of A # ) * the Arity of S)
by A2, A3, FUNCT_1:21;
( dom {} = {} & rng {} = {} )
;
then reconsider b = {} as Function of {} ,{} by FUNCT_2:3;
thus dom (Den o,A) =
Args o,A
by FUNCT_2:def 1
.=
((the Sorts of A # ) * the Arity of S) . o
by MSUALG_1:def 9
.=
(the Sorts of A # ) . (the Arity of S . o)
by A4, FUNCT_1:22
.=
(the Sorts of A # ) . (the_arity_of o)
by MSUALG_1:def 6
.=
product (the Sorts of A * (the_arity_of o))
by PBOOLE:def 19
.=
product (the Sorts of A * b)
by A1, MSUALG_1:def 6
.=
{{} }
by CARD_3:19
; :: thesis: verum