let f1, f2 be Function of (ClOpers L),((ClosureSystems L) opp); :: thesis: ( ( for c being closure Function of L,L holds f1 . c = Image c ) & ( for c being closure Function of L,L holds f2 . c = Image c ) implies f1 = f2 )

assume that

A3: for c being closure Function of L,L holds f1 . c = Image c and

A4: for c being closure Function of L,L holds f2 . c = Image c ; :: thesis: f1 = f2

assume that

A3: for c being closure Function of L,L holds f1 . c = Image c and

A4: for c being closure Function of L,L holds f2 . c = Image c ; :: thesis: f1 = f2

now :: thesis: for x being Element of (ClOpers L) holds f1 . x = f2 . x

hence
f1 = f2
by FUNCT_2:63; :: thesis: verumlet x be Element of (ClOpers L); :: thesis: f1 . x = f2 . x

reconsider c = x as closure Function of L,L by Th10;

thus f1 . x = Image c by A3

.= f2 . x by A4 ; :: thesis: verum

end;reconsider c = x as closure Function of L,L by Th10;

thus f1 . x = Image c by A3

.= f2 . x by A4 ; :: thesis: verum