let f, g be Function; :: thesis: for x, y being set st [x,y] in [:(dom f),(dom g):] holds
[:f,g:] . (x,y) = [(f . x),(g . y)]
let x, y be set ; :: thesis: ( [x,y] in [:(dom f),(dom g):] implies [:f,g:] . (x,y) = [(f . x),(g . y)] )
assume [x,y] in [:(dom f),(dom g):] ; :: thesis: [:f,g:] . (x,y) = [(f . x),(g . y)]
then ( x in dom f & y in dom g ) by ZFMISC_1:87;
hence [:f,g:] . (x,y) = [(f . x),(g . y)] by Def9; :: thesis: verum