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 * (canFS A) & g = FB * (canFS B) holds
f ^ g = FAB * ((canFS A) ^ (canFS B))
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 * (canFS A) & g = FB * (canFS B) holds
f ^ g = FAB * ((canFS A) ^ (canFS B))
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 * (canFS A) & g = FB * (canFS B) holds
f ^ g = FAB * ((canFS A) ^ (canFS B))
let f, g be FinSequence; :: thesis: for FAB being A \/ B -defined Function st A misses B & FAB = FA +* FB & f = FA * (canFS A) & g = FB * (canFS B) holds
f ^ g = FAB * ((canFS A) ^ (canFS B))
let FAB be A \/ B -defined Function; :: thesis: ( A misses B & FAB = FA +* FB & f = FA * (canFS A) & g = FB * (canFS B) implies f ^ g = FAB * ((canFS A) ^ (canFS B)) )
assume A1: A misses B ; :: thesis: ( not FAB = FA +* FB or not f = FA * (canFS A) or not g = FB * (canFS B) or f ^ g = FAB * ((canFS A) ^ (canFS B)) )
assume A2: FAB = FA +* FB ; :: thesis: ( not f = FA * (canFS A) or not g = FB * (canFS B) or f ^ g = FAB * ((canFS A) ^ (canFS B)) )
assume A3: f = FA * (canFS A) ; :: thesis: ( not g = FB * (canFS B) or f ^ g = FAB * ((canFS A) ^ (canFS B)) )
assume A4: g = FB * (canFS B) ; :: thesis: f ^ g = FAB * ((canFS A) ^ (canFS B))
reconsider csAB = (canFS A) ^ (canFS B) as one-to-one onto FinSequence of A \/ B by Lm3, A1;
set fAB = FAB * ((canFS A) ^ (canFS B));
set cSA = canFS A;
set cSB = canFS B;
A5: ( A = dom FA & rng (canFS A) = A ) by FUNCT_2:def 3, PARTFUN1:def 2;
then A6: dom f = dom (canFS A) by A3, RELAT_1:27;
then A7: dom f = Seg (len (canFS A)) by FINSEQ_1:def 3;
A8: ( B = dom FB & rng (canFS B) = B ) by FUNCT_2:def 3, PARTFUN1:def 2;
then dom g = dom (canFS B) by A4, RELAT_1:27;
then A9: dom g = Seg (len (canFS B)) by FINSEQ_1:def 3;
A10: A \/ B = dom FAB by A2, FUNCT_4:def 1, A5, A8;
rng csAB = A \/ B by FUNCT_2:def 3;
then A11: dom (FAB * ((canFS A) ^ (canFS B))) = dom csAB by RELAT_1:27, A10;
then dom (FAB * ((canFS A) ^ (canFS B))) = Seg (len csAB) by FINSEQ_1:def 3;
then reconsider fAB = FAB * ((canFS A) ^ (canFS B)) as FinSequence by FINSEQ_1:def 2;
A12: dom fAB = Seg (card (A \/ B)) by A11, Lm3, A1
.= Seg ((card A) + (card B)) by A1, CARD_2:40
.= Seg ((len (canFS A)) + (card B)) by FINSEQ_1:93
.= Seg ((len (canFS A)) + (len (canFS B))) by FINSEQ_1:93
.= Seg ((len f) + (len (canFS B))) by A7, FINSEQ_1:def 3
.= Seg ((len f) + (len g)) by A9, FINSEQ_1:def 3 ;
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 A6, FINSEQ_1:26, TARSKI:def 3;
then A15: fAB . k = FAB . (csAB . k) by FUNCT_1:13;
A16: csAB . k = (canFS A) . k by A14, A6, FINSEQ_1:def 7;
not csAB . k in dom FB

proof

assume A17: csAB . k in dom FB ; :: thesis: contradiction
(canFS A) . k in rng (canFS A) by A14, A6, FUNCT_1:3;
then csAB . k in A /\ B by A16, A17, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

then FAB . (csAB . k) = FA . (csAB . k) by A2, FUNCT_4:11;
hence fAB . k = FA . ((canFS A) . k) by A15, A14, A6, FINSEQ_1:def 7
.= f . k by A3, A14, A6, FUNCT_1:13 ;
:: 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 (canFS A) = len f by A7, FINSEQ_1:def 3;
A20: k in dom (canFS B) by A4, RELAT_1:27, A8, A18;
then (len f) + k in dom csAB by A19, FINSEQ_1:28;
then A21: fAB . ((len f) + k) = FAB . (csAB . ((len f) + k)) by FUNCT_1:13;
csAB . ((len f) + k) = (canFS B) . k by A20, A19, FINSEQ_1:def 7;
hence fAB . ((len f) + k) = FB . ((canFS B) . k) by A21, A20, FUNCT_1:3, FUNCT_4:13, A2, A8
.= g . k by A4, A20, FUNCT_1:13 ;
:: thesis: verum

end;

hence f ^ g = FAB * ((canFS A) ^ (canFS B)) by FINSEQ_1:def 7, A12, A13; :: thesis: verum