let X be 1-sorted ; :: thesis: ( X is constituted-FinSeqs implies X is constituted-Functions )
assume A1: X is constituted-FinSeqs ; :: thesis: X is constituted-Functions
let a be Element of H₁(X); :: according to MONOID_0:def 1 :: thesis: a is Function
thus a is Function by A1, Def2; :: thesis: verum