let T be non empty 1-sorted ; :: thesis: for N being net of T
for J being net_set of the carrier of N,T
for i being Element of N
for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let N be net of T; :: thesis: for J being net_set of the carrier of N,T
for i being Element of N
for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let J be net_set of the carrier of N,T; :: thesis: for i being Element of N
for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let i be Element of N; :: thesis: for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let f be Element of (product J); :: thesis: for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let x be Element of (Iterated J); :: thesis: ( x = [i,f] implies (Iterated J) . x = the mapping of (J . i) . (f . i) )
assume x = [i,f] ; :: thesis: (Iterated J) . x = the mapping of (J . i) . (f . i)
hence (Iterated J) . x = the mapping of (Iterated J) . i,f
.= the mapping of (J . i) . (f . i) by Def16 ;
:: thesis: verum