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 ;

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

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

dom <:f,g:> = dom (<:g,f:> ~)
by A1, Def1;<: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;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

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