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:46
.= {} by A2 ;
then rng (F * (the_arity_of o)) = {} by RELAT_1:65;
then F * (the_arity_of o) is Function of {} ,{} by A4, FUNCT_2:3;
then A5: e1 in product (doms (F * (the_arity_of o))) by A1, CARD_3:19, FUNCT_6:32, TARSKI:def 1;
A6: F # e = (Frege (F * (the_arity_of o))) . e by A3, MSUALG_3:def 7
.= (F * (the_arity_of o)) .. e1 by A5, PRALG_2:def 8 ;
then reconsider fn = F # e as Function ;
A7: dom fn = {} by A4, A6, PRALG_1:def 17;
then Seg 0 = dom fn ;
then reconsider fin = F # e as FinSequence by FINSEQ_1:def 2;
thus F # e = {} by A7; :: thesis: verum