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 ijk = <*i,j,k*> as Element of 3 -tuples_on NAT by FINSEQ_2:124;
reconsider ff = f as non empty homogeneous quasi_total PartFunc of (NAT * ),NAT by Th20;
A1: arity ff = 2 by Def26;
then A2: dom (ff * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT by Lm8;
A3: ( dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) & dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT ) by A1, Lm8;
thus ((1,2)->(1,?,2) f) . <*i,j,k*> = f . (<:<*(3 proj 1),(3 proj 3)*>:> . ijk) by A2, FUNCT_1:22
.= f . <*((3 proj 1) . ijk),((3 proj 3) . ijk)*> by 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