let I be non empty set ; :: thesis: for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for x being Element of (product (Union F))
for i being Element of I holds x | (J . i) = ((prod2dprod F) . x) . i
let J be non-empty disjoint_valued ManySortedSet of I; :: thesis: for F being Group-Family of I,J
for x being Element of (product (Union F))
for i being Element of I holds x | (J . i) = ((prod2dprod F) . x) . i
let F be Group-Family of I,J; :: thesis: for x being Element of (product (Union F))
for i being Element of I holds x | (J . i) = ((prod2dprod F) . x) . i
set f1 = dprod2prod F;
set f2 = prod2dprod F;
let x be Element of (product (Union F)); :: thesis: for i being Element of I holds x | (J . i) = ((prod2dprod F) . x) . i
let i be Element of I; :: thesis: x | (J . i) = ((prod2dprod F) . x) . i
A2: rng (dprod2prod F) = the carrier of (product (Union F)) by FUNCT_2:def 3;
reconsider y = (prod2dprod F) . x as Element of (dprod F) ;
((prod2dprod F) . x) . i = ((dprod2prod F) . y) | (J . i) by Def10
.= x | (J . i) by A2, FUNCT_1:35 ;
hence x | (J . i) = ((prod2dprod F) . x) . i ; :: thesis: verum