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
now :: thesis: for x being Element of (ClOpers L) holds f1 . x = f2 . x
let 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;
hence f1 = f2 by FUNCT_2:63; :: thesis: verum