let x1, x2, x3, x4 be object ; :: thesis: ( <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> & <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )
thus <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> ; :: thesis: ( <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )
thus <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> by FINSEQ_1:32; :: thesis: ( <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )
hence <*x1,x2,x3,x4*> = <*x1*> ^ (<*x2*> ^ <*x3,x4*>) by FINSEQ_1:32
.= <*x1*> ^ <*x2,x3,x4*> by FINSEQ_1:43 ;
:: thesis: <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>
thus <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> ; :: thesis: verum