set p = la .--> a;
let x be object ; :: according to FUNCT_1:def 14 :: thesis: ( not x in dom (la .--> a) or (la .--> a) . x in (the_Values_of S) . x )
assume x in dom (la .--> a) ; :: thesis: (la .--> a) . x in (the_Values_of S) . x
then A2: x = la by TARSKI:def 1;
then (la .--> a) . x = a by FUNCOP_1:72;
hence (la .--> a) . x in (the_Values_of S) . x by A2; :: thesis: verum