let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty ManySortedSet of I
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 I; :: 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 2;

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:9; :: 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 that
A4: dom x = I and
A5: for i being Element of I holds x . i is Element of (J . i) ; :: thesis: x is Element of (product J)

now :: thesis: for i being object st i in dom (Carrier J) holds
x . i in (Carrier J) . i

let i be object ; :: 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 2;
A6: x . j is Element of (J . j) by A5;
ex R being 1-sorted st
( R = J . j & (Carrier J) . j = the carrier of R ) by PRALG_1:def 15;
hence x . i in (Carrier J) . i by A6; :: thesis: verum

end;

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