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