let D be non empty set ; :: thesis: for A being BinOp of D st A is commutative & A is associative holds
for f, g being non empty FinSequence
for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
let A be BinOp of D; :: thesis: ( A is commutative & A is associative implies for f, g being non empty FinSequence
for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G))) )
assume A1: ( A is commutative & A is associative ) ; :: thesis: for f, g being non empty FinSequence
for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
defpred S₁[ Nat] means for f, g being non empty FinSequence st $1 = len g holds
for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)));
A2: S₁[1]

proof

let f, g be non empty FinSequence; :: thesis: ( 1 = len g implies for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G))) )
assume A3: 1 = len g ; :: thesis: for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
let F be Function of (dom f),D; :: thesis: for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
let G be Function of (dom g),D; :: thesis: for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
let FG be Function of (dom (f ^ g)),D; :: thesis: ( f = F & g = G & f ^ g = FG implies A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G))) )
assume A4: ( f = F & g = G & f ^ g = FG ) ; :: thesis: A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
len (f ^ g) = (len f) + 1 by FINSEQ_1:22, A3;
then dom (f ^ g) = Seg ((len f) + 1) by FINSEQ_1:def 3;
then A5: ( dom (f ^ g) = (Seg (len f)) \/ {((len f) + 1)} & Seg (len f) = dom f ) by FINSEQ_1:9, FINSEQ_1:def 3;
(len f) + 1 in {((len f) + 1)} by TARSKI:def 1;
then reconsider L1 = (len f) + 1 as Element of dom (f ^ g) by A5, XBOOLE_0:def 3;
dom f c= dom (f ^ g) by FINSEQ_1:26;
then reconsider Df = dom f as Element of Fin (dom (f ^ g)) by FINSUB_1:def 5;
len f < (len f) + 1 by NAT_1:13;
then A6: not L1 in Df by A5, FINSEQ_1:1;
A7: g = <*(g . 1)*> by A3, FINSEQ_1:40;
A8: ( dom g = {1} & 1 in {1} ) by FINSEQ_1:2, A3, FINSEQ_1:def 3;
A9: FG | Df = F | (dom f) by A4;
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (Df,FG)),(FG . L1)) by SETWOP_2:2, A1, A6, A5
.= A . ((A $$ (Df,FG)),(A $$ (([#] (dom g)),G))) by A4, A7, A8, A1, SETWISEO:17
.= A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G))) by A9, A1, Th1 ;
hence A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G))) ; :: thesis: verum

end;

A10: for n being Nat st 1 <= n & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( 1 <= n & S₁[n] implies S₁[n + 1] )
assume that
A11: 1 <= n and
A12: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let f, g be non empty FinSequence; :: thesis: ( n + 1 = len g implies for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G))) )
assume A13: n + 1 = len g ; :: thesis: for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
let F be Function of (dom f),D; :: thesis: for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
let G be Function of (dom g),D; :: thesis: for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
let FG be Function of (dom (f ^ g)),D; :: thesis: ( f = F & g = G & f ^ g = FG implies A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G))) )
assume A14: ( f = F & g = G & f ^ g = FG ) ; :: thesis: A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
( rng f c= D & rng g c= D ) by A14, RELAT_1:def 19;
then reconsider f1 = f, g1 = g as FinSequence of D by FINSEQ_1:def 4;
n < n + 1 by NAT_1:13;
then A15: len (g | n) = n by FINSEQ_1:59, A13;
reconsider gn = g1 | n as non empty FinSequence of D by A11;
rng gn c= D ;
then reconsider Gn = gn as Function of (dom gn),D by FUNCT_2:2;
f1 ^ (g1 | n) = f ^ gn ;
then rng (f ^ gn) c= D by FINSEQ_1:def 4;
then reconsider fgn = f ^ gn as Function of (dom (f ^ gn)),D by FUNCT_2:2;
A16: g = gn ^ <*(g . (n + 1))*> by A13, FINSEQ_3:55;
<*(g . (n + 1))*> is FinSequence of D by A16, FINSEQ_1:36;
then rng <*(g . (n + 1))*> c= D by FINSEQ_1:def 4;
then reconsider gn1 = <*(g . (n + 1))*> as Function of (dom <*(g . (n + 1))*>),D by FUNCT_2:2;
A17: len <*(g . (n + 1))*> = 1 by FINSEQ_1:40;
g = gn ^ <*(g . (n + 1))*> by A13, FINSEQ_3:55;
then f ^ g = (f ^ gn) ^ <*(g . (n + 1))*> by FINSEQ_1:32;
hence A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom (f ^ gn))),fgn)),(A $$ (([#] (dom <*(g . (n + 1))*>)),gn1))) by A14, A17, A2
.= A . ((A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom gn)),Gn)))),(A $$ (([#] (dom <*(g . (n + 1))*>)),gn1))) by A14, A12, A15
.= A . ((A $$ (([#] (dom f)),F)),(A . ((A $$ (([#] (dom gn)),Gn)),(A $$ (([#] (dom <*(g . (n + 1))*>)),gn1))))) by A1, BINOP_1:def 3
.= A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G))) by A16, A14, A17, A2 ;
:: thesis: verum

end;

A18: for n being Nat st 1 <= n holds
S₁[n] from NAT_1:sch 8(A2, A10);
let f, g be non empty FinSequence; :: thesis: for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))
len g >= 1 by NAT_1:14;
hence for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G))) by A18; :: thesis: verum