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

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

then ( f . i in rng f & rng f c= PFuncs (A * ),A ) by FUNCT_1:12, RELAT_1:def 19;
then ( f . i is PartFunc of (A * ),A & i is Element of NAT ) by A1, PARTFUN1:120;
hence f . i is homogeneous by A1, Def4; :: thesis: verum

end;

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

let x be FinSequence; :: according to UNIALG_1:def 1 :: thesis: for y being FinSequence st x in dom (f . i) & y in dom (f . i) holds
len x = len y
thus for y being FinSequence st x in dom (f . i) & y in dom (f . i) holds
len x = len y by A2, FUNCT_1:def 4, RELAT_1:60; :: thesis: verum

end;

end;