let f be Function; :: thesis: for I being non empty set
for F being Group-Family of I st dom f = I & ( for i being Element of I holds f . i in F . i ) holds
f in product F
let I be non empty set ; :: thesis: for F being Group-Family of I st dom f = I & ( for i being Element of I holds f . i in F . i ) holds
f in product F
let F be Group-Family of I; :: thesis: ( dom f = I & ( for i being Element of I holds f . i in F . i ) implies f in product F )
assume A1: dom f = I ; :: thesis: ( ex i being Element of I st not f . i in F . i or f in product F )
assume A2: for i being Element of I holds f . i in F . i ; :: thesis: f in product F
A3: dom (Carrier F) = I by PARTFUN1:def 2;
for i being object st i in dom (Carrier F) holds
f . i in (Carrier F) . i

proof

let i be object ; :: thesis: ( i in dom (Carrier F) implies f . i in (Carrier F) . i )
assume i in dom (Carrier F) ; :: thesis: f . i in (Carrier F) . i
then reconsider ii = i as Element of I ;
f . i in F . ii by A2;
hence f . i in (Carrier F) . i by Th9; :: thesis: verum

end;

then f in product (Carrier F) by A1, A3, CARD_3:9;
hence f in product F by GROUP_7:def 2; :: thesis: verum