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 SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2)
let U be non empty set ; :: thesis: for u being Element of U
for q1, q2 being U -valued FinSequence holds (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2)
let u be Element of U; :: thesis: for q1, q2 being U -valued FinSequence holds (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2)
let q1, q2 be U -valued FinSequence; :: thesis: (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2)
set e = x SubstWith u;
set w1 = q1;
set w2 = q2;
set w = q1 ^ q2;
set W1 = (x,u) -SymbolSubstIn q1;
set W2 = (x,u) -SymbolSubstIn q2;
set W = (x,u) -SymbolSubstIn (q1 ^ q2);
( (x SubstWith u) . q1 = (x,u) -SymbolSubstIn q1 & (x SubstWith u) . q2 = (x,u) -SymbolSubstIn q2 & (x SubstWith u) . (q1 ^ q2) = (x,u) -SymbolSubstIn (q1 ^ q2) ) by Def22;
hence (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) by Lm45; :: thesis: verum