let a be set ; :: thesis: for p being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F holds
dom (F [:] p,a) = dom p
let p be FinSequence; :: thesis: for F being Function st [:(rng p),{a}:] c= dom F holds
dom (F [:] p,a) = dom p
let F be Function; :: thesis: ( [:(rng p),{a}:] c= dom F implies dom (F [:] p,a) = dom p )
assume A1: [:(rng p),{a}:] c= dom F ; :: thesis: dom (F [:] p,a) = dom p
set q = (dom p) --> a;
rng ((dom p) --> a) c= {a} by FUNCOP_1:19;
then ( rng <:p,((dom p) --> a):> c= [:(rng p),(rng ((dom p) --> a)):] & [:(rng p),(rng ((dom p) --> a)):] c= [:(rng p),{a}:] ) by FUNCT_3:71, ZFMISC_1:118;
then ( dom p = dom p & dom ((dom p) --> a) = dom p & rng <:p,((dom p) --> a):> c= [:(rng p),{a}:] ) by FUNCOP_1:19, XBOOLE_1:1;
then ( dom <:p,((dom p) --> a):> = dom p & F [:] p,a = F * <:p,((dom p) --> a):> & rng <:p,((dom p) --> a):> c= dom F ) by A1, FUNCOP_1:def 4, FUNCT_3:70, XBOOLE_1:1;
hence dom (F [:] p,a) = dom p by RELAT_1:46; :: thesis: verum