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)) by FUNCT_6:def 2;
A2: ( dom a = Seg (len a) & dom u = Seg (len u) ) by FINSEQ_1:def 3;
A3: len u = len a by Th20;
A4: 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 A2, Th20;
u . x is UnOp of (a . x) ;
hence x in u " (SubFuncs (rng u)) by A2, A3, FUNCT_6:19; :: thesis: verum

end;

u " (SubFuncs (rng u)) c= dom u by RELAT_1:132;
then A5: dom (doms u) = dom u by A1, A4, XBOOLE_0:def 10;

A6: 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 A2, Th20;
(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

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 A2, Th20;
(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, A3, A5, FUNCT_1:2; :: thesis: product (rngs u) c= product a
dom (rngs u) = u " (SubFuncs (rng u)) by FUNCT_6:def 3;
hence product (rngs u) c= product a by A1, A2, A3, A5, A6, CARD_3:27; :: thesis: verum