let n be Nat; :: thesis: for A being non empty set
for g being Function
for a being Element of A
for k being Nat st 1 <= k & k <= n holds
(a .--> g) . ((n |-> a) /. k) = g
let A be non empty set ; :: thesis: for g being Function
for a being Element of A
for k being Nat st 1 <= k & k <= n holds
(a .--> g) . ((n |-> a) /. k) = g
let g be Function; :: thesis: for a being Element of A
for k being Nat st 1 <= k & k <= n holds
(a .--> g) . ((n |-> a) /. k) = g
let a be Element of A; :: thesis: for k being Nat st 1 <= k & k <= n holds
(a .--> g) . ((n |-> a) /. k) = g
let k be Nat; :: thesis: ( 1 <= k & k <= n implies (a .--> g) . ((n |-> a) /. k) = g )
assume ( 1 <= k & k <= n ) ; :: thesis: (a .--> g) . ((n |-> a) /. k) = g
then A1: k in Seg n by FINSEQ_1:1;
then k in dom (n |-> a) ;
then (n |-> a) /. k = (n |-> a) . k by PARTFUN1:def 6
.= a by A1, FUNCOP_1:7 ;
hence (a .--> g) . ((n |-> a) /. k) = g by FUNCOP_1:72; :: thesis: verum