let f1, f2 be Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X); :: thesis: ( ( for g being continuous Function of X,Sierpinski_Space holds f1 . g = g " {1} ) & ( for g being continuous Function of X,Sierpinski_Space holds f2 . g = g " {1} ) implies f1 = f2 )
assume that
A6: for g being continuous Function of X,Sierpinski_Space holds f1 . g = g " {1} and
A7: for g being continuous Function of X,Sierpinski_Space holds f2 . g = g " {1} ; :: thesis: f1 = f2

now :: thesis: for x being Element of (oContMaps (X,Sierpinski_Space)) holds f1 . x = f2 . x

let x be Element of (oContMaps (X,Sierpinski_Space)); :: thesis: f1 . x = f2 . x
reconsider g = x as continuous Function of X,Sierpinski_Space by WAYBEL26:2;
thus f1 . x = g " {1} by A6
.= f2 . x by A7 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum