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