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:44;
then A1: (<*x,y*> +* (2,z)) . 1 = x by FUNCT_7:32;
<*x,y*> . 2 = y by FINSEQ_1:44;
then A2: (<*x,y*> +* (1,z)) . 2 = y by FUNCT_7:32;
A3: len <*x,y*> = 2 by FINSEQ_1:44;
then 1 in dom <*x,y*> by FINSEQ_3:25;
then A4: (<*x,y*> +* (1,z)) . 1 = z by FUNCT_7:31;
len (<*x,y*> +* (1,z)) = 2 by A3, FUNCT_7:97;
hence <*x,y*> +* (1,z) = <*z,y*> by A4, A2, FINSEQ_1:44; :: thesis: <*x,y*> +* (2,z) = <*x,z*>
2 in dom <*x,y*> by A3, FINSEQ_3:25;
then A5: (<*x,y*> +* (2,z)) . 2 = z by FUNCT_7:31;
len (<*x,y*> +* (2,z)) = 2 by A3, FUNCT_7:97;
hence <*x,y*> +* (2,z) = <*x,z*> by A1, A5, FINSEQ_1:44; :: thesis: verum