let I be non empty set ; :: thesis: for F being Group-Family of I
for A being ManySortedSet of I st ( for i being Element of I holds A . i is Subset of (F . i) ) holds
product A is Subset of (product F)
let F be Group-Family of I; :: thesis: for A being ManySortedSet of I st ( for i being Element of I holds A . i is Subset of (F . i) ) holds
product A is Subset of (product F)
let A be ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is Subset of (F . i) ) implies product A is Subset of (product F) )
assume A1: for i being Element of I holds A . i is Subset of (F . i) ; :: thesis: product A is Subset of (product F)
for x being object st x in product A holds
x in the carrier of (product F)

proof

let x be object ; :: thesis: ( x in product A implies x in the carrier of (product F) )
assume B1: x in product A ; :: thesis: x in the carrier of (product F)
reconsider x = x as Function by B1;
B2: dom x = dom A by B1, CARD_3:9;
B3: ( dom F = I & dom A = I ) by PARTFUN1:def 2;
for i being Element of I holds x . i in F . i

proof

let i be Element of I; :: thesis: x . i in F . i
C1: A . i is Subset of (F . i) by A1;
x . i in A . i by B1, B3, CARD_3:9;
hence x . i in F . i by C1; :: thesis: verum

end;

then x in product F by B2, Th47, PARTFUN1:def 2;
hence x in the carrier of (product F) ; :: thesis: verum

end;

hence product A is Subset of (product F) by TARSKI:def 3; :: thesis: verum