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