let f, g be Function; :: thesis: <:f,g:> = <:g,f:> ~
A1: dom <:f,g:> = (dom g) /\ (dom f) by FUNCT_3:def 8
.= dom <:g,f:> by FUNCT_3:def 8 ;
then A2: dom <:f,g:> = dom (<:g,f:> ~ ) by Def1;

now

let x be set ; :: thesis: ( x in dom <:f,g:> implies <:f,g:> . x = (<:g,f:> ~ ) . x )
assume A3: x in dom <:f,g:> ; :: thesis: <:f,g:> . x = (<:g,f:> ~ ) . x
then A4: <:g,f:> . x = [(g . x),(f . x)] by A1, FUNCT_3:def 8;
thus <:f,g:> . x = [(f . x),(g . x)] by A3, FUNCT_3:def 8
.= (<:g,f:> ~ ) . x by A1, A3, A4, Def1 ; :: thesis: verum

end;

hence <:f,g:> = <:g,f:> ~ by A2, FUNCT_1:9; :: thesis: verum