set f = {} ;
( dom {} c= X * & rng {} c= Y ) by XBOOLE_1:2;
then reconsider f = {} as PartFunc of (X * ),Y by RELSET_1:11;
take f ; :: thesis: f is homogeneous
let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( not x in dom f or not y in dom f or len x = len y )
assume ( x in dom f & y in dom f ) ; :: thesis: len x = len y
hence len x = len y ; :: thesis: verum