let x be Element of Args (o,A); :: thesis: x is FinSequence-like
dom x = dom (the_arity_of o) by MSUALG_6:2;
then consider n being Nat such that
A1: dom x = Seg n by FINSEQ_1:def 2;
take n ; :: according to FINSEQ_1:def 2 :: thesis: dom x = Seg n
thus dom x = Seg n by A1; :: thesis: verum