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

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

hence
f1 = f2
by FUNCT_2:63; :: thesis: verumlet 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;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