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 )
A1: ( dom (doms u) = u " (SubFuncs (rng u)) & dom (rngs u) = u " (SubFuncs (rng u)) & dom a = Seg (len a) & dom u = Seg (len u) & len u = len a ) by Th20, FINSEQ_1:def 3, FUNCT_6:def 2, FUNCT_6:def 3;
A2: dom u c= u " (SubFuncs (rng u))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom u or x in u " (SubFuncs (rng u)) )
assume x in dom u ; :: thesis: x in u " (SubFuncs (rng u))
then reconsider x = x as Element of dom a by A1;
u . x is UnOp of (a . x) ;
hence x in u " (SubFuncs (rng u)) by A1, FUNCT_6:28; :: thesis: verum

end;

u " (SubFuncs (rng u)) c= dom u by RELAT_1:167;
then A3: dom (doms u) = dom u by A1, A2, XBOOLE_0:def 10;

now

let x be set ; :: 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 A1;
(doms u) . i = dom (u . i) by A1, FUNCT_6:31
.= a . i by FUNCT_2:def 1 ;
hence (doms u) . x = a . x ; :: thesis: verum

end;

hence doms u = a by A1, A3, FUNCT_1:9; :: thesis: product (rngs u) c= product a

now

let x be set ; :: 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 A1;
( (rngs u) . i = rng (u . i) & rng (u . i) c= a . i ) by A1, FUNCT_6:31, RELAT_1:def 19;
hence (rngs u) . x c= a . x ; :: thesis: verum

end;

hence product (rngs u) c= product a by A1, A3, CARD_3:38; :: thesis: verum