let A, B be non empty finite set ; :: thesis: for FA being A -defined total Function
for FB being B -defined total Function
for f, g being FinSequence
for FAB being A \/ B -defined Function st A misses B & FAB = FA +* FB & f = FA * () & g = FB * () holds
f ^ g = FAB * (() ^ ())

let FA be A -defined total Function; :: thesis: for FB being B -defined total Function
for f, g being FinSequence
for FAB being A \/ B -defined Function st A misses B & FAB = FA +* FB & f = FA * () & g = FB * () holds
f ^ g = FAB * (() ^ ())

let FB be B -defined total Function; :: thesis: for f, g being FinSequence
for FAB being A \/ B -defined Function st A misses B & FAB = FA +* FB & f = FA * () & g = FB * () holds
f ^ g = FAB * (() ^ ())

let f, g be FinSequence; :: thesis: for FAB being A \/ B -defined Function st A misses B & FAB = FA +* FB & f = FA * () & g = FB * () holds
f ^ g = FAB * (() ^ ())

let FAB be A \/ B -defined Function; :: thesis: ( A misses B & FAB = FA +* FB & f = FA * () & g = FB * () implies f ^ g = FAB * (() ^ ()) )
assume A1: A misses B ; :: thesis: ( not FAB = FA +* FB or not f = FA * () or not g = FB * () or f ^ g = FAB * (() ^ ()) )
assume A2: FAB = FA +* FB ; :: thesis: ( not f = FA * () or not g = FB * () or f ^ g = FAB * (() ^ ()) )
assume A3: f = FA * () ; :: thesis: ( not g = FB * () or f ^ g = FAB * (() ^ ()) )
assume A4: g = FB * () ; :: thesis: f ^ g = FAB * (() ^ ())
reconsider csAB = () ^ () as one-to-one onto FinSequence of A \/ B by ;
set fAB = FAB * (() ^ ());
set cSA = canFS A;
set cSB = canFS B;
A5: ( A = dom FA & rng () = A ) by ;
then A6: dom f = dom () by ;
then A7: dom f = Seg (len ()) by FINSEQ_1:def 3;
A8: ( B = dom FB & rng () = B ) by ;
then dom g = dom () by ;
then A9: dom g = Seg (len ()) by FINSEQ_1:def 3;
A10: A \/ B = dom FAB by ;
rng csAB = A \/ B by FUNCT_2:def 3;
then A11: dom (FAB * (() ^ ())) = dom csAB by ;
then dom (FAB * (() ^ ())) = Seg (len csAB) by FINSEQ_1:def 3;
then reconsider fAB = FAB * (() ^ ()) as FinSequence by FINSEQ_1:def 2;
A12: dom fAB = Seg (card (A \/ B)) by A11, Lm3, A1
.= Seg ((card A) + (card B)) by
.= Seg ((len ()) + (card B)) by FINSEQ_1:93
.= Seg ((len ()) + (len ())) by FINSEQ_1:93
.= Seg ((len f) + (len ())) by
.= Seg ((len f) + (len g)) by ;
A13: for k being Nat st k in dom f holds
fAB . k = f . k
proof
let k be Nat; :: thesis: ( k in dom f implies fAB . k = f . k )
assume A14: k in dom f ; :: thesis: fAB . k = f . k
then k in dom csAB by ;
then A15: fAB . k = FAB . (csAB . k) by FUNCT_1:13;
A16: csAB . k = () . k by ;
not csAB . k in dom FB
proof
assume A17: csAB . k in dom FB ; :: thesis: contradiction
(canFS A) . k in rng () by ;
then csAB . k in A /\ B by ;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum
end;
then FAB . (csAB . k) = FA . (csAB . k) by ;
hence fAB . k = FA . (() . k) by
.= f . k by ;
:: thesis: verum
end;
for k being Nat st k in dom g holds
fAB . ((len f) + k) = g . k
proof
let k be Nat; :: thesis: ( k in dom g implies fAB . ((len f) + k) = g . k )
assume A18: k in dom g ; :: thesis: fAB . ((len f) + k) = g . k
A19: len () = len f by ;
A20: k in dom () by ;
then (len f) + k in dom csAB by ;
then A21: fAB . ((len f) + k) = FAB . (csAB . ((len f) + k)) by FUNCT_1:13;
csAB . ((len f) + k) = () . k by ;
hence fAB . ((len f) + k) = FB . (() . k) by
.= g . k by ;
:: thesis: verum
end;
hence f ^ g = FAB * (() ^ ()) by ; :: thesis: verum