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

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