let IT1, IT2 be Function of (U *),(U *); :: thesis: ( ( for q being U -valued FinSequence holds IT1 . q = (x,u) -SymbolSubstIn q ) & ( for q being U -valued FinSequence holds IT2 . q = (x,u) -SymbolSubstIn q ) implies IT1 = IT2 )
assume A2: for q being U -valued FinSequence holds IT1 . q = (x,u) -SymbolSubstIn q ; :: thesis: ( ex q being U -valued FinSequence st not IT2 . q = (x,u) -SymbolSubstIn q or IT1 = IT2 )
assume A3: for q being U -valued FinSequence holds IT2 . q = (x,u) -SymbolSubstIn q ; :: thesis: IT1 = IT2

now :: thesis: for w being Element of U * holds IT1 . w = IT2 . w

let w be Element of U * ; :: thesis: IT1 . w = IT2 . w
thus IT1 . w = H₁(w) by A2
.= IT2 . w by A3 ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum