let x, y be Element of BOOLEAN ; :: thesis: ( inv1 . <*(xor2 . <*x,y*>)*> = xor2a . <*x,y*> & inv1 . <*(xor2 . <*x,y*>)*> = xor2c . <*x,y*> & xor2 . <*(inv1 . <*x*>),(inv1 . <*y*>)*> = xor2 . <*x,y*> )
thus inv1 . <*(xor2 . <*x,y*>)*> = inv1 . <*(x 'xor' y)*> by FACIRC_1:def 4
.= 'not' (x 'xor' y) by Def1
.= ('not' x) 'xor' y by XBOOLEAN:74
.= xor2a . <*x,y*> by TWOSCOMP:def 14 ; :: thesis: ( inv1 . <*(xor2 . <*x,y*>)*> = xor2c . <*x,y*> & xor2 . <*(inv1 . <*x*>),(inv1 . <*y*>)*> = xor2 . <*x,y*> )
hence inv1 . <*(xor2 . <*x,y*>)*> = xor2c . <*x,y*> by Th4; :: thesis: xor2 . <*(inv1 . <*x*>),(inv1 . <*y*>)*> = xor2 . <*x,y*>
thus xor2 . <*(inv1 . <*x*>),(inv1 . <*y*>)*> = xor2 . <*('not' x),(inv1 . <*y*>)*> by Th1
.= xor2 . <*('not' x),('not' y)*> by Th1
.= ('not' x) 'xor' ('not' y) by FACIRC_1:def 4
.= x 'xor' y
.= xor2 . <*x,y*> by FACIRC_1:def 4 ; :: thesis: verum