let i, j, k be Element of NAT ; 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; ((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 ijk = <*i,j,k*> 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,(ijk . 3)*>
by FINSEQ_1:45
.=
f . <*i,k*>
by FINSEQ_1:45
;
verum