( dom {} = {} & rng {} = {} )
;
then reconsider b = {} as Function of {},{} by FUNCT_2:1;
let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for o being OperSymbol of S st the Arity of S . o = {} holds
dom (Den (o,A)) = {{}}
let A be non-empty MSAlgebra over S; for o being OperSymbol of S st the Arity of S . o = {} holds
dom (Den (o,A)) = {{}}
let o be OperSymbol of S; ( the Arity of S . o = {} implies dom (Den (o,A)) = {{}} )
assume A1:
the Arity of S . o = {}
; dom (Den (o,A)) = {{}}
A2:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
then
( dom ( the Sorts of A #) = the carrier of S * & the Arity of S . o in rng the Arity of S )
by FUNCT_1:def 3, PARTFUN1:def 2;
then A3:
o in dom (( the Sorts of A #) * the Arity of S)
by A2, FUNCT_1:11;
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 4
.=
( the Sorts of A #) . ( the Arity of S . o)
by A3, FUNCT_1:12
.=
( the Sorts of A #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product ( the Sorts of A * (the_arity_of o))
by FINSEQ_2:def 5
.=
product ( the Sorts of A * b)
by A1, MSUALG_1:def 1
.=
{{}}
by CARD_3:10
; verum