let E be Element of F; :: thesis: ( E is finite & E is Function-like & E is Relation-like )

per cases ( F = {} or F <> {} ) ;

suppose F = {} ; :: thesis: ( E is finite & E is Function-like & E is Relation-like )

hence ( E is finite & E is Function-like & E is Relation-like ) ; :: thesis: verum

end;

suppose F <> {} ; :: thesis: ( E is finite & E is Function-like & E is Relation-like )

hence ( E is finite & E is Function-like & E is Relation-like ) by Def7; :: thesis: verum

end;

end;