let D be set ; :: thesis: for f, g being FinSequence of D * holds Values (f ^ g) = (Values f) \/ (Values g)
let f, g be FinSequence of D * ; :: thesis: Values (f ^ g) = (Values f) \/ (Values g)
set F = f ^ g;
A1: Values f c= Values (f ^ g)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Values f or a in Values (f ^ g) )
assume a in Values f ; :: thesis: a in Values (f ^ g)
then consider x, y being object such that
A2: ( x in dom f & y in dom (f . x) & a = (f . x) . y ) by Th1;
reconsider x = x as Nat by A2;
A3: dom f c= dom (f ^ g) by FINSEQ_1:26;
f . x = (f ^ g) . x by A2, FINSEQ_1:def 7;
hence a in Values (f ^ g) by A3, A2, Th1; :: thesis: verum

end;

A4: Values g c= Values (f ^ g)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Values g or a in Values (f ^ g) )
assume a in Values g ; :: thesis: a in Values (f ^ g)
then consider x, y being object such that
A5: ( x in dom g & y in dom (g . x) & a = (g . x) . y ) by Th1;
reconsider x = x as Nat by A5;
( (len f) + x in dom (f ^ g) & (f ^ g) . ((len f) + x) = g . x ) by A5, FINSEQ_1:28, FINSEQ_1:def 7;
hence a in Values (f ^ g) by A5, Th1; :: thesis: verum

end;

Values (f ^ g) c= (Values f) \/ (Values g)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Values (f ^ g) or a in (Values f) \/ (Values g) )
assume a in Values (f ^ g) ; :: thesis: a in (Values f) \/ (Values g)
then consider x, y being object such that
A6: ( x in dom (f ^ g) & y in dom ((f ^ g) . x) & a = ((f ^ g) . x) . y ) by Th1;
reconsider x = x as Nat by A6;

per cases ( x in dom f or ex k being Nat st
( k in dom g & x = (len f) + k ) ) by A6, FINSEQ_1:25;

suppose A7: x in dom f ; :: thesis: a in (Values f) \/ (Values g)

then f . x = (f ^ g) . x by FINSEQ_1:def 7;
then a in Values f by Th1, A6, A7;
hence a in (Values f) \/ (Values g) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom g & x = (len f) + k ) ; :: thesis: a in (Values f) \/ (Values g)

then consider k being Nat such that
A8: ( k in dom g & x = (len f) + k ) ;
(f ^ g) . x = g . k by A8, FINSEQ_1:def 7;
then a in Values g by Th1, A6, A8;
hence a in (Values f) \/ (Values g) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence Values (f ^ g) = (Values f) \/ (Values g) by A1, A4, XBOOLE_1:8; :: thesis: verum