let x be set ; :: thesis: for U being non empty set
for u being Element of U
for q1, q2 being b₁ -valued FinSequence holds (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2)
let U be non empty set ; :: thesis: for u being Element of U
for q1, q2 being U -valued FinSequence holds (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2)
let u be Element of U; :: thesis: for q1, q2 being U -valued FinSequence holds (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2)
let q1, q2 be U -valued FinSequence; :: thesis: (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2)
set s1 = x;
set s2 = u;
set w1 = q1;
set w2 = q2;
set w = q1 ^ q2;
set IT1 = (x,u) -SymbolSubstIn q1;
set IT2 = (x,u) -SymbolSubstIn q2;
set IT = (x,u) -SymbolSubstIn (q1 ^ q2);
set f = x .--> u;
set I = id U;
reconsider g = (id U) +* (x,u) as Function of U,U ;
reconsider w11 = q1, w22 = q2, ww = q1 ^ q2 as FinSequence of U by Lm45;
thus (x,u) -SymbolSubstIn (q1 ^ q2) = (g * w11) ^ (g * w22) by FINSEQOP:9
.= ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2) ; :: thesis: verum