let x be set ; :: thesis: for U being non empty set
for u being Element of U
for p being FinSequence st p is U * -valued holds
(x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p)
let U be non empty set ; :: thesis: for u being Element of U
for p being FinSequence st p is U * -valued holds
(x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p)
let u be Element of U; :: thesis: for p being FinSequence st p is U * -valued holds
(x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p)
let p be FinSequence; :: thesis: ( p is U * -valued implies (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) )
set S = U;
set C = U -multiCat ;
set SS = U;
set strings = U * ;
set e = x SubstWith u;
set m = len p;
set F = U -firstChar ;
set FF = (U *) -firstChar ;
set g = U -concatenation ;
set G = MultPlace (U -concatenation);
defpred S₁[ Nat] means for p being U * -valued $1 -element FinSequence holds (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p);
B10: S₁[ 0 ] ;
B11: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
assume C0: S₁[n] ; :: thesis: S₁[n + 1]
let p be U * -valued n + 1 -element FinSequence; :: thesis: (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p)
reconsider q = p | (Seg n) as U * -valued n -element FinSequence ;
q is n -element FinSequence of U * by Lm45;
then reconsider qq = q as n -element Element of (U *) * by FINSEQ_1:def 11;
p is (n + 1) + 0 -element ;
then {(p . (n + 1))} \ (U *) = {} ;
then reconsider z = p . (n + 1) as Element of U * by ZFMISC_1:60;
reconsider f = (x SubstWith u) . z as Element of U * ;
(q ^ <*z*>) \+\ p = {} ;
then C1: q ^ <*z*> = p by Th29;
(U -multiCat) . ((x SubstWith u) * p) = (U -multiCat) . (((x SubstWith u) * qq) ^ <*f*>) by C1, FINSEQOP:8
.= ((U -multiCat) . ((x SubstWith u) * qq)) ^ f by Th33
.= ((x SubstWith u) . ((U -multiCat) . qq)) ^ f by C0
.= (x SubstWith u) . (((U -multiCat) . qq) ^ z) by Lm55
.= (x SubstWith u) . ((U -multiCat) . p) by Th33, C1 ;
hence (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) ; :: thesis: verum

end;

B1: for n being Nat holds S₁[n] from NAT_1:sch 2(B10, B11);
assume p is U * -valued ; :: thesis: (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p)
then reconsider pp = p as U * -valued len p -element FinSequence by CARD_1:def 7;
(x SubstWith u) . ((U -multiCat) . pp) = (U -multiCat) . ((x SubstWith u) * pp) by B1;
hence (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) ; :: thesis: verum