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 S1[ Nat] means for p being U * -valued $1 -element FinSequence holds (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p);
A1: S1[ 0 ] ;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set n1 = n + 1;
assume A3: S1[n] ; :: thesis: S1[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 ;
reconsider qq = q as n -element FinSequence of U * by Lm1;
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 A4: q ^ <*z*> = p by Th29;
(U -multiCat) . ((x SubstWith u) * p) = (U -multiCat) . (((x SubstWith u) * qq) ^ <*f*>) by FINSEQOP:8, A4
.= ((U -multiCat) . ((x SubstWith u) * qq)) ^ f by Th33
.= ((x SubstWith u) . ((U -multiCat) . qq)) ^ f by A3
.= (x SubstWith u) . (((U -multiCat) . qq) ^ z) by Lm47
.= (x SubstWith u) . ((U -multiCat) . p) by Th33, A4 ;
hence (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) ; :: thesis: verum
end;
A5: for n being Nat holds S1[n] from NAT_1:sch 2(A1, A2);
 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 A5;
hence (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) ; :: thesis: verum