set f = p .--> x;
thus not p .--> x is empty ; :: thesis: p .--> x is homogeneous
thus dom (p .--> x) is with_common_domain :: according to MARGREL1:def 22 :: thesis: verum

proof

let x, y be Function; :: according to CARD_3:def 10 :: thesis: ( not x in dom (p .--> x) or not y in dom (p .--> x) or proj1 x = proj1 y )
assume that
A1: x in dom (p .--> x) and
A2: y in dom (p .--> x) ; :: thesis: proj1 x = proj1 y
A3: dom (p .--> x) = {p} by FUNCOP_1:19;
then x = p by A1, TARSKI:def 1;
hence proj1 x = proj1 y by A3, A2, TARSKI:def 1; :: thesis: verum

end;