<:g,f:> = <:f,g:> ~ by FUNCOP_1:2;
hence <:g,f:> is one-to-one ; :: thesis: verum