let a, b be object ; :: thesis: for f, g being FinSequence holds Swap ((f ^ g),a,b) = (Swap (f,a,b)) ^ (Swap (g,a,b))
let f, g be FinSequence; :: thesis: Swap ((f ^ g),a,b) = (Swap (f,a,b)) ^ (Swap (g,a,b))
set Sf = Swap (f,a,b);
set Sg = Swap (g,a,b);
set Sfg = Swap ((f ^ g),a,b);
A1: ( len (Swap (f,a,b)) = len f & len (Swap (g,a,b)) = len g & len (Swap ((f ^ g),a,b)) = len (f ^ g) ) by CARD_1:def 7;
A2: ( len ((Swap (f,a,b)) ^ (Swap (g,a,b))) = (len (Swap (f,a,b))) + (len (Swap (g,a,b))) & len (f ^ g) = (len f) + (len g) ) by FINSEQ_1:22;
for k being Nat st 1 <= k & k <= len (Swap ((f ^ g),a,b)) holds
(Swap ((f ^ g),a,b)) . k = ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (Swap ((f ^ g),a,b)) implies (Swap ((f ^ g),a,b)) . k = ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k )
assume A3: ( 1 <= k & k <= len (Swap ((f ^ g),a,b)) ) ; :: thesis: (Swap ((f ^ g),a,b)) . k = ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k
A4: k in dom (f ^ g) by A3, A1, FINSEQ_3:25;

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

suppose A5: k in dom f ; :: thesis: (Swap ((f ^ g),a,b)) . k = ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k

then A6: f . k = (f ^ g) . k by FINSEQ_1:def 7;
A7: dom f c= dom (f ^ g) by FINSEQ_1:26;
k in dom (Swap (f,a,b)) by A5, Def4;
then A8: ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k = (Swap (f,a,b)) . k by FINSEQ_1:def 7;

per cases ( a in f . k or not a in f . k ) ;

suppose A9: a in f . k ; :: thesis: (Swap ((f ^ g),a,b)) . k = ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k

hence ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k = ((f . k) \ {a}) \/ {b} by A8, A5, Def4
.= (Swap ((f ^ g),a,b)) . k by A6, A9, A7, A5, Def4 ;
:: thesis: verum

end;

suppose A10: not a in f . k ; :: thesis: (Swap ((f ^ g),a,b)) . k = ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k

hence ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k = (f . k) \/ {a} by A8, A5, Def4
.= (Swap ((f ^ g),a,b)) . k by A6, A10, A7, A5, Def4 ;
:: thesis: verum

end;

end;

end;

suppose ex n being Nat st
( n in dom g & k = (len f) + n ) ; :: thesis: (Swap ((f ^ g),a,b)) . k = ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k

then consider n being Nat such that
A11: ( n in dom g & k = (len f) + n ) ;
A12: g . n = (f ^ g) . k by A11, FINSEQ_1:def 7;
n in dom (Swap (g,a,b)) by A11, Def4;
then A13: ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k = (Swap (g,a,b)) . n by A11, A1, FINSEQ_1:def 7;

per cases ( a in g . n or not a in g . n ) ;

suppose A14: a in g . n ; :: thesis: (Swap ((f ^ g),a,b)) . k = ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k

hence ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k = ((g . n) \ {a}) \/ {b} by A13, A11, Def4
.= (Swap ((f ^ g),a,b)) . k by A12, A14, A4, Def4 ;
:: thesis: verum

end;

suppose A15: not a in g . n ; :: thesis: (Swap ((f ^ g),a,b)) . k = ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k

hence ((Swap (f,a,b)) ^ (Swap (g,a,b))) . k = (g . n) \/ {a} by A13, A11, Def4
.= (Swap ((f ^ g),a,b)) . k by A12, A15, A4, Def4 ;
:: thesis: verum

end;

end;

end;

end;

end;

hence Swap ((f ^ g),a,b) = (Swap (f,a,b)) ^ (Swap (g,a,b)) by A2, A1; :: thesis: verum