per cases ( i in dom f or not i in dom f ) ;
suppose i in dom f ; :: thesis: f . i is homogeneous
hence f . i is homogeneous by Def23; :: thesis: verum
end;
suppose not i in dom f ; :: thesis: f . i is homogeneous
hence f . i is homogeneous by FUNCT_1:def 2, RELAT_1:38; :: thesis: verum
end;
end;