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