let a be object ; 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; for F being Function st [:{a},(rng p):] c= dom F holds
dom (F [;] (a,p)) = dom p
let F be Function; ( [:{a},(rng p):] c= dom F implies dom (F [;] (a,p)) = dom p )
assume A1:
[:{a},(rng p):] c= dom F
; 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; verum