let i, j, k be Element of NAT ; :: thesis: for f being NAT * -defined to-naturals homogeneous len-total binary Function holds ((1,2)->(1,?,2) f) . <*i,j,k*> = f . <*i,k*>
let f be NAT * -defined to-naturals homogeneous len-total binary Function; :: thesis: ((1,2)->(1,?,2) f) . <*i,j,k*> = f . <*i,k*>
reconsider ff = f as non empty homogeneous quasi_total PartFunc of (NAT * ),NAT by Th20;
reconsider ijk = <*i,j,k*> as Element of 3 -tuples_on NAT by FINSEQ_2:124;
A1: arity ff = 2 by Def26;
then A2: dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) by Lm8;
A3: dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT by A1, Lm8;
dom (ff * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT by A1, Lm8;
hence ((1,2)->(1,?,2) f) . <*i,j,k*> = f . (<:<*(3 proj 1),(3 proj 3)*>:> . ijk) by FUNCT_1:22
.= f . <*((3 proj 1) . ijk),((3 proj 3) . ijk)*> by A2, A3, FUNCT_6:62
.= f . <*(ijk . 1),((3 proj 3) . ijk)*> by Th42
.= f . <*(ijk . 1),(ijk . 3)*> by Th42
.= f . <*i,(ijk . 3)*> by FINSEQ_1:62
.= f . <*i,k*> by FINSEQ_1:62 ;
:: thesis: verum