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

A2: now :: thesis: for x being object st x in dom <:f,g:> holds
<:f,g:> . x = (<:g,f:> ~) . x

let x be object ; :: 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 7;
thus <:f,g:> . x = [(f . x),(g . x)] by A3, FUNCT_3:def 7
.= (<:g,f:> ~) . x by A1, A3, A4, Def1 ; :: thesis: verum

end;

dom <:f,g:> = dom (<:g,f:> ~) by A1, Def1;
hence <:f,g:> = <:g,f:> ~ by A2; :: thesis: verum