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;
dom ((dom p) --> a) = dom p by FUNCOP_1:19;
then A2: dom <:p,((dom p) --> a):> = dom p by FUNCT_3:70;
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 A3: rng <:p,((dom p) --> a):> c= [:(rng p),{a}:] by XBOOLE_1:1;
F [:] p,a = F * <:p,((dom p) --> a):> by FUNCOP_1:def 4;
hence dom (F [:] p,a) = dom p by A1, A3, A2, RELAT_1:46, XBOOLE_1:1; :: thesis: verum