:: deftheorem Def23 defines homogeneous MARGREL1:def 23 :
for A being set
for IT being PFuncFinSequence of A holds
( IT is homogeneous iff for n being Nat
for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds
h is homogeneous );