set f = the FinSequence;
take X = 1-sorted(# { the FinSequence} #); :: thesis: X is constituted-FinSeqs
let a be Element of X; :: according to MONOID_0:def 2 :: thesis: a is FinSequence
thus a is FinSequence by TARSKI:def 1; :: thesis: verum