reconsider f = I --> {{}} as Function ;
reconsider f = f as ManySortedSet of I ;
take f ; :: thesis: ( f is V2() & f is V44() )
thus f is V2() ; :: thesis: f is V44()
thus f is V44() by FUNCOP_1:7; :: thesis: verum