per cases ( i in dom f or not i in dom f ) ;

suppose A1: i in dom f ; :: thesis: f . i is homogeneous

A2: rng f c= PFuncs ((A *),A) by RELAT_1:def 19;
f . i in rng f by A1, FUNCT_1:3;
then f . i is PartFunc of (A *),A by A2, PARTFUN1:46;
hence f . i is homogeneous by A1, Def24; :: thesis: verum

end;

suppose A3: not i in dom f ; :: thesis: f . i is homogeneous

let x be Function; :: according to CARD_3:def 10,MARGREL1:def 21 :: thesis: for b₁ being set holds
( not x in dom (f . i) or not b₁ in dom (f . i) or proj1 x = proj1 b₁ )
thus for b₁ being set holds
( not x in dom (f . i) or not b₁ in dom (f . i) or proj1 x = proj1 b₁ ) by A3, FUNCT_1:def 2, RELAT_1:38; :: thesis: verum

end;

end;