:: deftheorem Def3 defines ^^ LTLAXIO3:def 3 :
for X being set
for f, g being one-to-one FinSequence of X st rng f misses rng g holds
f ^^ g = f ^ g;