let x, y be Surreal; :: thesis: for X1, X2, Y being set holds comp ((X1 \/ X2),x,y,Y) = (comp (X1,x,y,Y)) \/ (comp (X2,x,y,Y))
let X1, X2, Y be set ; :: thesis: comp ((X1 \/ X2),x,y,Y) = (comp (X1,x,y,Y)) \/ (comp (X2,x,y,Y))
comp ((X1 \/ X2),x,y,Y) = comp (Y,y,x,(X1 \/ X2)) by Th53
.= (comp (Y,y,x,X1)) \/ (comp (Y,y,x,X2)) by Th60
.= (comp (X1,x,y,Y)) \/ (comp (Y,y,x,X2)) by Th53 ;
hence comp ((X1 \/ X2),x,y,Y) = (comp (X1,x,y,Y)) \/ (comp (X2,x,y,Y)) by Th53; :: thesis: verum