take the one-to-one Function ; :: thesis: the one-to-one Function is oneone
thus the one-to-one Function is oneone ; :: thesis: verum