let T be non empty 1-sorted ; :: thesis: for N being net of
for J being net_set of the carrier of N,T
for i being Element of
for f being Element of
for x being Element of st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let N be net of ; :: thesis: for J being net_set of the carrier of N,T
for i being Element of
for f being Element of
for x being Element of 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
for f being Element of
for x being Element of st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let i be Element of ; :: thesis: for f being Element of
for x being Element of st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let f be Element of ; :: thesis: for x being Element of st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let x be Element of ; :: 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