let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty ManySortedSet of
for x being Function holds
( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )
let J be RelStr-yielding non-Empty ManySortedSet of ; :: thesis: for x being Function holds
( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )
let x be Function; :: thesis: ( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )
A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def 4;
A2: dom (Carrier J) = I by PARTFUN1:def 4;

hereby :: thesis: ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) implies x is Element of (product J) )

assume A3: x is Element of (product J) ; :: thesis: ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) )
hence dom x = I by A1, A2, CARD_3:18; :: thesis: for i being Element of I holds x . i is Element of (J . i)
let i be Element of I; :: thesis: x . i is Element of (J . i)
reconsider y = x as Element of (product J) by A3;
y . i is Element of (J . i) ;
hence x . i is Element of (J . i) ; :: thesis: verum

end;

assume A4: ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) ; :: thesis: x is Element of (product J)

now

let i be set ; :: thesis: ( i in dom (Carrier J) implies x . i in (Carrier J) . i )
assume i in dom (Carrier J) ; :: thesis: x . i in (Carrier J) . i
then reconsider j = i as Element of I by PARTFUN1:def 4;
x . j is Element of (J . j) by A4;
then ( x . j in the carrier of (J . j) & ex R being 1-sorted st
( R = J . j & (Carrier J) . j = the carrier of R ) ) by PRALG_1:def 13;
hence x . i in (Carrier J) . i ; :: thesis: verum

end;

hence x is Element of (product J) by A1, A2, A4, CARD_3:18; :: thesis: verum