let D1, D2 be non empty set ; :: thesis: for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 * st f1 = f2 holds
(D1 -concatenation) "**" f1 = (D2 -concatenation) "**" f2
let f1 be FinSequence of D1 * ; :: thesis: for f2 being FinSequence of D2 * st f1 = f2 holds
(D1 -concatenation) "**" f1 = (D2 -concatenation) "**" f2
let f2 be FinSequence of D2 * ; :: thesis: ( f1 = f2 implies (D1 -concatenation) "**" f1 = (D2 -concatenation) "**" f2 )
set CC = D2 -concatenation ;
set NC = D1 -concatenation ;
defpred S₁[ Nat] means for fn being FinSequence of D1 *
for fc being FinSequence of D2 * st $1 = len fn & fn = fc holds
(D1 -concatenation) "**" fn = (D2 -concatenation) "**" fc;
A1: S₁[ 0 ]

proof

let fn be FinSequence of D1 * ; :: thesis: for fc being FinSequence of D2 * st 0 = len fn & fn = fc holds
(D1 -concatenation) "**" fn = (D2 -concatenation) "**" fc
let fc be FinSequence of D2 * ; :: thesis: ( 0 = len fn & fn = fc implies (D1 -concatenation) "**" fn = (D2 -concatenation) "**" fc )
assume ( 0 = len fn & fn = fc ) ; :: thesis: (D1 -concatenation) "**" fn = (D2 -concatenation) "**" fc
then ( fn = {} & fc = {} ) ;
then ( (D1 -concatenation) "**" fn = {} & (D2 -concatenation) "**" fc = {} ) by Lm1;
hence (D1 -concatenation) "**" fn = (D2 -concatenation) "**" fc ; :: thesis: verum

end;

A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
let fn be FinSequence of D1 * ; :: thesis: for fc being FinSequence of D2 * st i + 1 = len fn & fn = fc holds
(D1 -concatenation) "**" fn = (D2 -concatenation) "**" fc
let fc be FinSequence of D2 * ; :: thesis: ( i + 1 = len fn & fn = fc implies (D1 -concatenation) "**" fn = (D2 -concatenation) "**" fc )
assume A4: ( i + 1 = len fn & fn = fc ) ; :: thesis: (D1 -concatenation) "**" fn = (D2 -concatenation) "**" fc
then consider f1 being FinSequence of D1 * , d1 being Element of D1 * such that
A5: fn = f1 ^ <*d1*> by FINSEQ_2:19;
consider f2 being FinSequence of D2 * , d2 being Element of D2 * such that
A6: fc = f2 ^ <*d2*> by FINSEQ_2:19, A4;
A7: (len f1) + 1 = len fn by A5, FINSEQ_2:16;
A8: (D2 -concatenation) "**" fc = ((D2 -concatenation) "**" f2) ^ ((D2 -concatenation) "**" <*d2*>) by Th3, A6
.= ((D2 -concatenation) "**" f2) ^ d2 by FINSOP_1:11 ;
A9: (D1 -concatenation) "**" fn = ((D1 -concatenation) "**" f1) ^ ((D1 -concatenation) "**" <*d1*>) by Th3, A5
.= ((D1 -concatenation) "**" f1) ^ d1 by FINSOP_1:11 ;
( f1 = f2 & d1 = d2 ) by A5, A6, A4, FINSEQ_2:17;
hence (D1 -concatenation) "**" fn = (D2 -concatenation) "**" fc by A3, A7, A4, A8, A9; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence ( f1 = f2 implies (D1 -concatenation) "**" f1 = (D2 -concatenation) "**" f2 ) ; :: thesis: verum