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;
<*x,y*> . 1 = x by FINSEQ_1:61;
then A1: (<*x,y*> +* 2,z) . 1 = x by FUNCT_7:34;
<*x,y*> . 2 = y by FINSEQ_1:61;
then A2: (<*x,y*> +* 1,z) . 2 = y by FUNCT_7:34;
A3: len <*x,y*> = 2 by FINSEQ_1:61;
then 1 in dom <*x,y*> by FINSEQ_3:27;
then A4: (<*x,y*> +* 1,z) . 1 = z by FUNCT_7:33;
len (<*x,y*> +* 1,z) = 2 by A3, FUNCT_7:99;
hence <*x,y*> +* 1,z = <*z,y*> by A4, A2, FINSEQ_1:61; :: thesis: <*x,y*> +* 2,z = <*x,z*>
2 in dom <*x,y*> by A3, FINSEQ_3:27;
then A5: (<*x,y*> +* 2,z) . 2 = z by FUNCT_7:33;
len (<*x,y*> +* 2,z) = 2 by A3, FUNCT_7:99;
hence <*x,y*> +* 2,z = <*x,z*> by A1, A5, FINSEQ_1:61; :: thesis: verum