:: deftheorem Def6 defines J/A-independent COMPOS_0:def 7 :
for S being non empty standard-ins set holds
( S is J/A-independent iff for T being InsType of S
for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds
for p being object st [T,f1,p] in S holds
[T,f2,p] in S );