let a be object ; :: 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 ;
then A2: dom <:p,((dom p) --> a):> = dom p by FUNCT_3:50;
rng ((dom p) --> a) c= {a} by FUNCOP_1:13;
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:51, ZFMISC_1:95;
then A3: rng <:p,((dom p) --> a):> c= [:(rng p),{a}:] ;
thus dom (F [:] (p,a)) = dom p by A1, A3, A2, RELAT_1:27, XBOOLE_1:1; :: thesis: verum