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 holds rng ((dprod2prod F) | (dsum F)) = [#] (sum (Union F))
let J be non-empty disjoint_valued ManySortedSet of I; :: thesis: for F being Group-Family of I,J holds rng ((dprod2prod F) | (dsum F)) = [#] (sum (Union F))
let F be Group-Family of I,J; :: thesis: rng ((dprod2prod F) | (dsum F)) = [#] (sum (Union F))
for y being object holds
( y in rng ((dprod2prod F) | ([#] (dsum F))) iff y in [#] (sum (Union F)) )
proof
let y be object ; :: thesis: ( y in rng ((dprod2prod F) | ([#] (dsum F))) iff y in [#] (sum (Union F)) )
A1: dom (dprod2prod F) = [#] (dprod F) by FUNCT_2:def 1;
hereby :: thesis: ( y in [#] (sum (Union F)) implies y in rng ((dprod2prod F) | ([#] (dsum F))) )
assume y in rng ((dprod2prod F) | ([#] (dsum F))) ; :: thesis: y in [#] (sum (Union F))
then consider x being object such that
A2: ( x in dom ((dprod2prod F) | ([#] (dsum F))) & y = ((dprod2prod F) | ([#] (dsum F))) . x ) by FUNCT_1:def 3;
x in (dom (dprod2prod F)) /\ ([#] (dsum F)) by A2, RELAT_1:61;
then A3: ( x in dom (dprod2prod F) & x in [#] (dsum F) ) by XBOOLE_0:def 4;
reconsider x = x as Function by A2;
( x in dprod F & x in dsum F ) by A3;
then (dprod2prod F) . x in sum (Union F) by Th32;
hence y in [#] (sum (Union F)) by A2, FUNCT_1:47; :: thesis: verum
end;
assume A4: y in [#] (sum (Union F)) ; :: thesis: y in rng ((dprod2prod F) | ([#] (dsum F)))
then reconsider y0 = y as Element of (sum (Union F)) ;
y0 in [#] (product (Union F)) by GROUP_2:def 5, TARSKI:def 3;
then reconsider y0 = y as Element of (product (Union F)) ;
y0 in sum (Union F) by A4;
then consider x being Function such that
A5: y0 = (dprod2prod F) . x and
A6: x in dsum F by Th31;
A7: y = ((dprod2prod F) | ([#] (dsum F))) . x by A5, A6, FUNCT_1:49;
x in dom ((dprod2prod F) | ([#] (dsum F))) by A1, A6, GROUP_2:def 5, RELAT_1:62;
hence y in rng ((dprod2prod F) | ([#] (dsum F))) by A7, FUNCT_1:3; :: thesis: verum
end;
hence rng ((dprod2prod F) | (dsum F)) = [#] (sum (Union F)) by TARSKI:2; :: thesis: verum