let f, g be Function; <: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 for x being object st x in dom <:f,g:> holds
<:f,g:> . x = (<:g,f:> ~) . xlet x be
object ;
( x in dom <:f,g:> implies <:f,g:> . x = (<:g,f:> ~) . x )assume A3:
x in dom <:f,g:>
;
<:f,g:> . x = (<:g,f:> ~) . xthen 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
;
verum end;
dom <:f,g:> = dom (<:g,f:> ~)
by A1, Def1;
hence
<:f,g:> = <:g,f:> ~
by A2; verum