let f, g be Function; for A being set holds <:f,g:> | A = <:(f | A),g:>
let A be set ; <:f,g:> | A = <:(f | A),g:>
A1: dom (<:f,g:> | A) =
(dom <:f,g:>) /\ A
by RELAT_1:61
.=
((dom f) /\ (dom g)) /\ A
by FUNCT_3:def 7
.=
((dom f) /\ A) /\ (dom g)
by XBOOLE_1:16
.=
(dom (f | A)) /\ (dom g)
by RELAT_1:61
;
now for x being object st x in dom (<:f,g:> | A) holds
(<:f,g:> | A) . x = [((f | A) . x),(g . x)]A2:
dom (<:f,g:> | A) c= dom <:f,g:>
by RELAT_1:60;
let x be
object ;
( x in dom (<:f,g:> | A) implies (<:f,g:> | A) . x = [((f | A) . x),(g . x)] )assume A3:
x in dom (<:f,g:> | A)
;
(<:f,g:> | A) . x = [((f | A) . x),(g . x)]A4:
x in dom (f | A)
by A1, A3, XBOOLE_0:def 4;
thus (<:f,g:> | A) . x =
<:f,g:> . x
by A3, FUNCT_1:47
.=
[(f . x),(g . x)]
by A3, A2, FUNCT_3:def 7
.=
[((f | A) . x),(g . x)]
by A4, FUNCT_1:47
;
verum end;
hence
<:f,g:> | A = <:(f | A),g:>
by A1, FUNCT_3:def 7; verum