let x, x9, y, y9 be object ; :: 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 Th54;
hence |:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] by Def3; :: thesis: verum