let x, y, z be set ; :: thesis: ( <*x,y*> +* 1,z = <*z,y*> & <*x,y*> +* 2,z = <*x,z*> )
set a = <*x,y*> +* 1,z;
set b = <*x,y*> +* 2,z;
A1: ( len <*x,y*> = 2 & <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by FINSEQ_1:61;
then A2: ( 1 in dom <*x,y*> & 2 in dom <*x,y*> ) by FINSEQ_3:27;
then ( len (<*x,y*> +* 1,z) = 2 & (<*x,y*> +* 1,z) . 1 = z & (<*x,y*> +* 1,z) . 2 = y ) by A1, FUNCT_7:33, FUNCT_7:34, JORDAN2B:12;
hence <*x,y*> +* 1,z = <*z,y*> by FINSEQ_1:61; :: thesis: <*x,y*> +* 2,z = <*x,z*>
( len (<*x,y*> +* 2,z) = 2 & (<*x,y*> +* 2,z) . 1 = x & (<*x,y*> +* 2,z) . 2 = z ) by A1, A2, FUNCT_7:33, FUNCT_7:34, JORDAN2B:12;
hence <*x,y*> +* 2,z = <*x,z*> by FINSEQ_1:61; :: thesis: verum