deffunc H₁( 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 H₁(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) = H₁(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 ; :: thesis: ( 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):] ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum