let x1, x2, x3, y1, y2, y3 be set ; :: thesis: [:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
thus [:{x1,x2,x3},{y1,y2,y3}:] = [:({x1} \/ {x2,x3}),{y1,y2,y3}:] by ENUMSET1:2
.= [:({x1} \/ {x2,x3}),({y1} \/ {y2,y3}):] by ENUMSET1:2
.= (([:{x1},{y1}:] \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ [:{x2,x3},{y2,y3}:] by ZFMISC_1:98
.= (([:{x1},{y1}:] \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:109
.= (({[x1,y1]} \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:29
.= (({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30
.= (({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30
.= (({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30
.= (({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ZFMISC_1:30
.= ({[x1,y1],[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:2
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:9
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ {[x2,y2],[x2,y3],[x3,y2],[x3,y3]} by ENUMSET1:5
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1],[x2,y2],[x2,y3],[x3,y2],[x3,y3]} by ENUMSET1:81
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x3,y1],[x2,y2],[x2,y3],[x3,y2],[x3,y3]} by ENUMSET1:80
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x3,y1],[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:9
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x2,y2],[x2,y3],[x3,y1]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:59
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]} by ENUMSET1:9
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]} by ENUMSET1:80 ; :: thesis: verum