let S be non empty non void ManySortedSign ; for U1, U2 being MSAlgebra over S
for o being OperSymbol of S
for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds
for F being ManySortedFunction of U1,U2 holds F # e = {}
let U1, U2 be MSAlgebra over S; for o being OperSymbol of S
for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds
for F being ManySortedFunction of U1,U2 holds F # e = {}
let o be OperSymbol of S; for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds
for F being ManySortedFunction of U1,U2 holds F # e = {}
let e be Element of Args (o,U1); ( e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} implies for F being ManySortedFunction of U1,U2 holds F # e = {} )
assume that
A1:
e = {}
and
A2:
the_arity_of o = {}
and
A3:
( Args (o,U1) <> {} & Args (o,U2) <> {} )
; for F being ManySortedFunction of U1,U2 holds F # e = {}
reconsider e1 = e as Function by A1;
let F be ManySortedFunction of U1,U2; F # e = {}
A4:
dom (F * (the_arity_of o)) = {}
by A2;
then
rng (F * (the_arity_of o)) = {}
by RELAT_1:42;
then
F * (the_arity_of o) is Function of {},{}
by A4, FUNCT_2:1;
then A5:
e1 in product (doms (F * (the_arity_of o)))
by A1, CARD_3:10, FUNCT_6:23, TARSKI:def 1;
A6: F # e =
(Frege (F * (the_arity_of o))) . e
by A3, MSUALG_3:def 5
.=
(F * (the_arity_of o)) .. e1
by A5, PRALG_2:def 2
;
then reconsider fn = F # e as Function ;
dom fn = {} /\ (dom e1)
by A4, A6, PRALG_1:def 19;
hence
F # e = {}
; verum