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