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 ;

now :: thesis: 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 ; :: 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;

hence <:f,g:> | A = <:(f | A),g:> by A1, FUNCT_3:def 7; :: thesis: verum