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 = {} & the_arity_of o = {} ) and
A2: ( Args o,U1 <> {} & Args o,U2 <> {} ) ; :: thesis: for F being ManySortedFunction of U1,U2 holds F # e = {}
let F be ManySortedFunction of U1,U2; :: thesis: F # e = {}
reconsider e1 = e as Function by A1;
rng (the_arity_of o) = {} by A1;
then rng (the_arity_of o) c= dom F by XBOOLE_1:2;
then A3: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46
.= {} by A1 ;
then rng (F * (the_arity_of o)) = {} by RELAT_1:65;
then F * (the_arity_of o) is Function of {} ,{} by A3, FUNCT_2:3;
then product (doms (F * (the_arity_of o))) = {{} } by CARD_3:19, FUNCT_6:32;
then A4: e1 in product (doms (F * (the_arity_of o))) by A1, TARSKI:def 1;
A5: F # e = (Frege (F * (the_arity_of o))) . e by A2, MSUALG_3:def 7
.= (F * (the_arity_of o)) .. e1 by A4, PRALG_2:def 8 ;
then reconsider fn = F # e as Function ;
A6: dom fn = {} by A3, A5, PRALG_1:def 17;
then reconsider fin = F # e as FinSequence by FINSEQ_1:4, FINSEQ_1:def 2;
fin = {} by A6;
hence F # e = {} ; :: thesis: verum