let f, g be Function; :: thesis: for A being set holds <:f,g:> | A = <:(f | A),g:>

let A be set ; :: thesis: <: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 ;

let A be set ; :: thesis: <: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 :: thesis: for x being object st x in dom (<:f,g:> | A) holds

(<:f,g:> | A) . x = [((f | A) . x),(g . x)]

hence
<:f,g:> | A = <:(f | A),g:>
by A1, FUNCT_3:def 7; :: thesis: verum(<: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 ; :: thesis: ( x in dom (<:f,g:> | A) implies (<:f,g:> | A) . x = [((f | A) . x),(g . x)] )

assume A3: x in dom (<:f,g:> | A) ; :: thesis: (<: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 ; :: thesis: verum

end;let x be object ; :: thesis: ( x in dom (<:f,g:> | A) implies (<:f,g:> | A) . x = [((f | A) . x),(g . x)] )

assume A3: x in dom (<:f,g:> | A) ; :: thesis: (<: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 ; :: thesis: verum