set p = la .--> a;
A2: dom (la .--> a) = {la} by FUNCOP_1:13;
let x be set ; :: according to FUNCT_1:def 14 :: thesis: ( not x in proj1 (la .--> a) or (la .--> a) . x in the Object-Kind of S . x )
assume x in dom (la .--> a) ; :: thesis: (la .--> a) . x in the Object-Kind of S . x
then A4: x = la by A2, TARSKI:def 1;
then (la .--> a) . x = a by FUNCOP_1:72;
hence (la .--> a) . x in the Object-Kind of S . x by A4; :: thesis: verum