let F be FinSequence-yielding FinSequence; :: thesis: for g being FinSequence
for x being object holds doms (F ^ <*(g ^ <*x*>)*>) = (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F }
let g be FinSequence; :: thesis: for x being object holds doms (F ^ <*(g ^ <*x*>)*>) = (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F }
let x be object ; :: thesis: doms (F ^ <*(g ^ <*x*>)*>) = (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F }
set S = { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } ;
set gx = g ^ <*x*>;
A1: ( len (F ^ <*(g ^ <*x*>)*>) = 1 + (len F) & len (F ^ <*g*>) = 1 + (len F) ) by FINSEQ_2:16;
thus doms (F ^ <*(g ^ <*x*>)*>) c= (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } :: according to XBOOLE_0:def 10 :: thesis: (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } c= doms (F ^ <*(g ^ <*x*>)*>)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in doms (F ^ <*(g ^ <*x*>)*>) or y in (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } )
assume y in doms (F ^ <*(g ^ <*x*>)*>) ; :: thesis: y in (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F }
then consider p being FinSequence such that
A2: ( p = y & len p = len (F ^ <*(g ^ <*x*>)*>) ) and
A3: for i being Nat st i in dom p holds
p . i in dom ((F ^ <*(g ^ <*x*>)*>) . i) by Def8;

per cases ( p . (1 + (len F)) in dom g or not p . (1 + (len F)) in dom g ) ;

suppose A4: p . (1 + (len F)) in dom g ; :: thesis: y in (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F }

for i being Nat st i in dom p holds
p . i in dom ((F ^ <*g*>) . i)

proof

let i be Nat; :: thesis: ( i in dom p implies p . i in dom ((F ^ <*g*>) . i) )
assume A5: i in dom p ; :: thesis: p . i in dom ((F ^ <*g*>) . i)

per cases ( i = 1 + (len F) or i <> 1 + (len F) ) ;

suppose i = 1 + (len F) ; :: thesis: p . i in dom ((F ^ <*g*>) . i)

hence p . i in dom ((F ^ <*g*>) . i) by A4; :: thesis: verum

end;

suppose A6: i <> 1 + (len F) ; :: thesis: p . i in dom ((F ^ <*g*>) . i)

A7: ( 1 <= i & i <= len p ) by A5, FINSEQ_3:25;
then i < (len F) + 1 by A6, A2, A1, XXREAL_0:1;
then i <= len F by NAT_1:13;
then i in dom F by A7, FINSEQ_3:25;
then ( (F ^ <*(g ^ <*x*>)*>) . i = F . i & (F ^ <*g*>) . i = F . i ) by FINSEQ_1:def 7;
hence p . i in dom ((F ^ <*g*>) . i) by A5, A3; :: thesis: verum

end;

end;

end;

then p in doms (F ^ <*g*>) by A2, A1, Th47;
hence y in (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } by A2, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A8: not p . (1 + (len F)) in dom g ; :: thesis: y in (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F }

1 <= 1 + (len F) by NAT_1:11;
then p . (1 + (len F)) in dom ((F ^ <*(g ^ <*x*>)*>) . (1 + (len F))) by A3, A2, A1, FINSEQ_3:25;
then consider n being Nat such that
A9: ( n in dom <*x*> & p . (1 + (len F)) = (len g) + n ) by A8, FINSEQ_1:25;
set pL = p | (len F);
n in Seg 1 by A9, FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def 1;
then A10: p = (p | (len F)) ^ <*(1 + (len g))*> by A9, FINSEQ_3:55, A2, FINSEQ_2:16;
A11: len (p | (len F)) = len F by A2, A1, FINSEQ_3:53;
for i being Nat st i in dom (p | (len F)) holds
(p | (len F)) . i in dom (F . i)

proof

let i be Nat; :: thesis: ( i in dom (p | (len F)) implies (p | (len F)) . i in dom (F . i) )
assume A12: i in dom (p | (len F)) ; :: thesis: (p | (len F)) . i in dom (F . i)
dom F = Seg (len F) by FINSEQ_1:def 3;
then A13: ( i in dom p & i in dom F ) by A12, RELAT_1:57;
then p . i in dom ((F ^ <*(g ^ <*x*>)*>) . i) by A3;
then p . i in dom (F . i) by A13, FINSEQ_1:def 7;
hence (p | (len F)) . i in dom (F . i) by A12, FUNCT_1:47; :: thesis: verum

end;

then p | (len F) in doms F by A11, Th47;
then p in { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } by A10;
hence y in (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } or y in doms (F ^ <*(g ^ <*x*>)*>) )
assume A14: y in (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } ; :: thesis: y in doms (F ^ <*(g ^ <*x*>)*>)
set L = 1 + (len g);

per cases ( y in { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } or not y in { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } ) ;

suppose y in { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } ; :: thesis: y in doms (F ^ <*(g ^ <*x*>)*>)

then consider f being Element of doms F such that
A15: ( y = f ^ <*(1 + (len g))*> & f in doms F ) ;
A16: ( len f = len F & len (f ^ <*(1 + (len g))*>) = (len f) + 1 & len (g ^ <*x*>) = 1 + (len g) ) by A15, Th47, FINSEQ_2:16;
then A17: dom f = dom F by FINSEQ_3:30;
for i being Nat st i in dom (f ^ <*(1 + (len g))*>) holds
(f ^ <*(1 + (len g))*>) . i in dom ((F ^ <*(g ^ <*x*>)*>) . i)

proof

let i be Nat; :: thesis: ( i in dom (f ^ <*(1 + (len g))*>) implies (f ^ <*(1 + (len g))*>) . i in dom ((F ^ <*(g ^ <*x*>)*>) . i) )
assume A18: i in dom (f ^ <*(1 + (len g))*>) ; :: thesis: (f ^ <*(1 + (len g))*>) . i in dom ((F ^ <*(g ^ <*x*>)*>) . i)

per cases ( i in dom f or ex n being Nat st
( n in dom <*(1 + (len g))*> & i = (len f) + n ) ) by A18, FINSEQ_1:25;

suppose i in dom f ; :: thesis: (f ^ <*(1 + (len g))*>) . i in dom ((F ^ <*(g ^ <*x*>)*>) . i)

then ( f . i in dom (F . i) & (f ^ <*(1 + (len g))*>) . i = f . i & (F ^ <*(g ^ <*x*>)*>) . i = F . i ) by A17, A15, Th47, FINSEQ_1:def 7;
hence (f ^ <*(1 + (len g))*>) . i in dom ((F ^ <*(g ^ <*x*>)*>) . i) ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom <*(1 + (len g))*> & i = (len f) + n ) ; :: thesis: (f ^ <*(1 + (len g))*>) . i in dom ((F ^ <*(g ^ <*x*>)*>) . i)

then consider n being Nat such that
A19: ( n in dom <*(1 + (len g))*> & i = (len f) + n ) ;
A20: 1 <= 1 + (len g) by NAT_1:11;
n in Seg 1 by A19, FINSEQ_1:def 8;
then n = 1 by TARSKI:def 1, FINSEQ_1:2;
hence (f ^ <*(1 + (len g))*>) . i in dom ((F ^ <*(g ^ <*x*>)*>) . i) by A19, A16, FINSEQ_3:25, A20; :: thesis: verum

end;

end;

end;

hence y in doms (F ^ <*(g ^ <*x*>)*>) by A15, A16, A1, Th47; :: thesis: verum

end;

suppose not y in { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F } ; :: thesis: y in doms (F ^ <*(g ^ <*x*>)*>)

then y in doms (F ^ <*g*>) by A14, XBOOLE_0:def 3;
then consider p being FinSequence such that
A21: ( p = y & len p = len (F ^ <*g*>) ) and
A22: for i being Nat st i in dom p holds
p . i in dom ((F ^ <*g*>) . i) by Def8;
A23: dom p = dom (F ^ <*g*>) by A21, FINSEQ_3:30;
for i being Nat st i in dom p holds
p . i in dom ((F ^ <*(g ^ <*x*>)*>) . i)

proof

let i be Nat; :: thesis: ( i in dom p implies p . i in dom ((F ^ <*(g ^ <*x*>)*>) . i) )
assume A24: i in dom p ; :: thesis: p . i in dom ((F ^ <*(g ^ <*x*>)*>) . i)

per cases ( i in dom F or not i in dom F ) ;

suppose i in dom F ; :: thesis: p . i in dom ((F ^ <*(g ^ <*x*>)*>) . i)

then ( (F ^ <*g*>) . i = F . i & F . i = (F ^ <*(g ^ <*x*>)*>) . i ) by FINSEQ_1:def 7;
hence p . i in dom ((F ^ <*(g ^ <*x*>)*>) . i) by A24, A22; :: thesis: verum

end;

suppose not i in dom F ; :: thesis: p . i in dom ((F ^ <*(g ^ <*x*>)*>) . i)

then consider n being Nat such that
A25: ( n in dom <*g*> & i = (len F) + n ) by A24, A23, FINSEQ_1:25;
n in Seg 1 by A25, FINSEQ_1:38;
then A26: n = 1 by FINSEQ_1:2, TARSKI:def 1;
then (F ^ <*g*>) . i = g by A25;
then p . i in dom g by A24, A22;
hence p . i in dom ((F ^ <*(g ^ <*x*>)*>) . i) by A26, A25, FINSEQ_1:26, TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence y in doms (F ^ <*(g ^ <*x*>)*>) by A1, Th47, A21; :: thesis: verum

end;

end;