let a be object ; :: thesis: for p being FinSequence
for F being Function st [:{a},(rng p):] c= dom F holds
dom (F [;] (a,p)) = dom p
let p be FinSequence; :: thesis: for F being Function st [:{a},(rng p):] c= dom F holds
dom (F [;] (a,p)) = dom p
let F be Function; :: thesis: ( [:{a},(rng p):] c= dom F implies dom (F [;] (a,p)) = dom p )
assume A1: [:{a},(rng p):] c= dom F ; :: thesis: dom (F [;] (a,p)) = dom p
set q = (dom p) --> a;
dom ((dom p) --> a) = dom p ;
then A2: dom <:((dom p) --> a),p:> = dom p by FUNCT_3:50;
rng ((dom p) --> a) c= {a} by FUNCOP_1:13;
then ( rng <:((dom p) --> a),p:> c= [:(rng ((dom p) --> a)),(rng p):] & [:(rng ((dom p) --> a)),(rng p):] c= [:{a},(rng p):] ) by FUNCT_3:51, ZFMISC_1:95;
then A3: rng <:((dom p) --> a),p:> c= [:{a},(rng p):] ;
thus dom (F [;] (a,p)) = dom p by A1, A3, A2, RELAT_1:27, XBOOLE_1:1; :: thesis: verum