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;

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

( 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

(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;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

now :: thesis: for x being object st x in dom u holds

(doms u) . x = a . x

hence
doms u = a
by A2, Th12, A4; :: thesis: product (rngs u) c= product a(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;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

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