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:12;
then f . i is PartFunc of , by A2, PARTFUN1:120;
hence f . i is homogeneous by A1, Def4; :: 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,UNIALG_1:def 1 :: thesis: for b₁ being set holds
( not x in dom (f . i) or not b₁ in dom (f . i) or dom x = dom b₁ )
thus for b₁ being set holds
( not x in dom (f . i) or not b₁ in dom (f . i) or dom x = dom b₁ ) by A3, FUNCT_1:def 4, RELAT_1:60; :: thesis: verum

end;

end;