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

fAB . ((len f) + k) = g . k

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

for k being Nat st k in dom g holds
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

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;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

then
FAB . (csAB . k) = FA . (csAB . k)
by A2, FUNCT_4:11;
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;(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

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

fAB . ((len f) + k) = g . k

proof

hence
f ^ g = FAB * ((canFS A) ^ (canFS B))
by FINSEQ_1:def 7, A12, A13; :: thesis: verum
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;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