let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being MSAlgebra of 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 of S; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) <> {} ) ; :: thesis: for F being ManySortedFunction of U1,U2 holds F # e = {}
reconsider e1 = e as Function by A1;
let F be ManySortedFunction of U1,U2; :: thesis: F # e = {}
rng (the_arity_of o) = {} by A2;
then rng (the_arity_of o) c= dom F by XBOOLE_1:2;
then A4: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27
.= {} 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 ;
A7: dom fn = {} by A4, A6, PRALG_1:def 17;
thus F # e = {} by A7; :: thesis: verum