let F be FinSequence-yielding FinSequence; :: thesis: for x being object holds doms (F ^ <*<*x*>*>) = { (f ^ <*1*>) where f is Element of doms F : f in doms F }
let x be object ; :: thesis: doms (F ^ <*<*x*>*>) = { (f ^ <*1*>) where f is Element of doms F : f in doms F }
( 1 <= (len F) + 1 & len (F ^ <*{}*>) = (len F) + 1 ) by FINSEQ_2:16, NAT_1:11;
then ( 1 + (len F) in dom (F ^ <*{}*>) & (F ^ <*{}*>) . (1 + (len F)) = {} ) by FINSEQ_3:25;
then not F ^ <*{}*> is non-empty ;
then A1: doms (F ^ <*{}*>) = {} by Th45;
reconsider g = {} as FinSequence ;
doms (F ^ <*(g ^ <*x*>)*>) = (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } by Th52;
hence doms (F ^ <*<*x*>*>) = { (f ^ <*1*>) where f is Element of doms F : f in doms F } by A1; :: thesis: verum