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:90
.= ((dom f) /\ (dom g)) /\ A by FUNCT_3:def 8
.= ((dom f) /\ A) /\ (dom g) by XBOOLE_1:16
.= (dom (f | A)) /\ (dom g) by RELAT_1:90 ;

now

let x be set ; :: thesis: ( x in dom (<:f,g:> | A) implies (<:f,g:> | A) . x = [((f | A) . x),(g . x)] )
assume A2: x in dom (<:f,g:> | A) ; :: thesis: (<:f,g:> | A) . x = [((f | A) . x),(g . x)]
A3: dom (<:f,g:> | A) c= dom <:f,g:> by RELAT_1:89;
A4: x in dom (f | A) by A1, A2, XBOOLE_0:def 4;
thus (<:f,g:> | A) . x = <:f,g:> . x by A2, FUNCT_1:70
.= [(f . x),(g . x)] by A2, A3, FUNCT_3:def 8
.= [((f | A) . x),(g . x)] by A4, FUNCT_1:70 ; :: thesis: verum

end;

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