let i, j, k be Nat; :: thesis: for f being NAT * -defined to-naturals homogeneous len-total 2 -ary Function holds ((1,2)->(1,?,2) f) . <*i,j,k*> = f . <*i,k*>
let f be NAT * -defined to-naturals homogeneous len-total 2 -ary 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 Th16;
reconsider i1 = i, j1 = j, k1 = k as Element of NAT by ORDINAL1:def 12;
reconsider ijk = <*i1,j1,k1*> as Element of 3 -tuples_on NAT by FINSEQ_2:104;
A1: arity ff = 2 by Def21;
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:12
.= f . <*((3 proj 1) . ijk),((3 proj 3) . ijk)*> by A2, A3, FINSEQ_3:142
.= f . <*(ijk . 1),((3 proj 3) . ijk)*> by Th37
.= f . <*(ijk . 1),(ijk . 3)*> by Th37
.= f . <*i,k*> ;
:: thesis: verum