let a be Domain-Sequence; :: thesis: for u being UnOps of a holds
( doms u = a & product (rngs u) c= product a )
let u be UnOps of a; :: thesis: ( doms u = a & product (rngs u) c= product a )
A2: ( dom a = Seg (len a) & dom u = Seg (len u) ) by FINSEQ_1:def 3;
A3: len u = len a by Th12;
A4: dom (doms u) = dom u by FUNCT_6:def 2;
A5: now :: thesis: for x being object st x in dom u holds
(rngs u) . x c= a . x
let x be object ; :: thesis: ( x in dom u implies (rngs u) . x c= a . x )
assume x in dom u ; :: thesis: (rngs u) . x c= a . x
then reconsider i = x as Element of dom a by A2, Th12;
(rngs u) . i = rng (u . i) by A2, A3, FUNCT_6:22;
hence (rngs u) . x c= a . x by RELAT_1:def 19; :: thesis: verum
end;
now :: thesis: for x being object st x in dom u holds
(doms u) . x = a . x
let x be object ; :: thesis: ( x in dom u implies (doms u) . x = a . x )
assume x in dom u ; :: thesis: (doms u) . x = a . x
then reconsider i = x as Element of dom a by A2, Th12;
(doms u) . i = dom (u . i) by A2, A3, FUNCT_6:22
.= a . i by FUNCT_2:def 1 ;
hence (doms u) . x = a . x ; :: thesis: verum
end;
hence doms u = a by A2, Th12, A4; :: thesis: product (rngs u) c= product a
dom (rngs u) = dom u by FUNCT_6:def 3;
hence product (rngs u) c= product a by A2, A3, A5, CARD_3:27; :: thesis: verum