deffunc H1( Element of Y, Element of (product J)) -> Element of the carrier of T = the mapping of (J . $1) . ($2 . $1);
set R = [:Y,(product J):];
A1:
for i being Element of Y
for f being Element of (product J) holds H1(i,f) in the carrier of T
;
consider F being Function of [: the carrier of Y, the carrier of (product J):],T such that
A2:
for i being Element of Y
for f being Element of (product J) holds F . (i,f) = H1(i,f)
from FUNCT_7:sch 1(A1);
the carrier of [:Y,(product J):] = [: the carrier of Y, the carrier of (product J):]
by YELLOW_3:def 2;
then reconsider F = F as Function of [:Y,(product J):],T ;
reconsider N = NetStr(# the carrier of [:Y,(product J):], the InternalRel of [:Y,(product J):],F #) as strict net of T by Lm1, Lm2;
take
N
; ( RelStr(# the carrier of N, the InternalRel of N #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of N . (i,f) = the mapping of (J . i) . (f . i) ) )
thus
RelStr(# the carrier of N, the InternalRel of N #) = [:Y,(product J):]
; for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of N . (i,f) = the mapping of (J . i) . (f . i)
let i be Element of Y; for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of N . (i,f) = the mapping of (J . i) . (f . i)
let f be Function; ( i in the carrier of Y & f in the carrier of (product J) implies the mapping of N . (i,f) = the mapping of (J . i) . (f . i) )
assume that
i in the carrier of Y
and
A3:
f in the carrier of (product J)
; the mapping of N . (i,f) = the mapping of (J . i) . (f . i)
thus
the mapping of N . (i,f) = the mapping of (J . i) . (f . i)
by A2, A3; verum