defpred S_{1}[ set , set ] means ex c being closure Function of L,L st

( c = $1 & $2 = Image c );

A2: for x being Element of (ClOpers L) holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

take f ; :: thesis: for c being closure Function of L,L holds f . c = Image c

let c be closure Function of L,L; :: thesis: f . c = Image c

c is Element of (ClOpers L) by Th10;

then ex c1 being closure Function of L,L st

( c1 = c & f . c = Image c1 ) by A2;

hence f . c = Image c ; :: thesis: verum

( c = $1 & $2 = Image c );

A1: now :: thesis: for x being Element of (ClOpers L) ex b being Element of the carrier of ((ClosureSystems L) ~) st S_{1}[x,b]

consider f being Function of (ClOpers L),((ClosureSystems L) opp) such that let x be Element of (ClOpers L); :: thesis: ex b being Element of the carrier of ((ClosureSystems L) ~) st S_{1}[x,b]

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

reconsider a = Image c as Element of (ClosureSystems L) by Th16;

take b = a ~ ; :: thesis: S_{1}[x,b]

thus S_{1}[x,b]
; :: thesis: verum

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

reconsider a = Image c as Element of (ClosureSystems L) by Th16;

take b = a ~ ; :: thesis: S

thus S

A2: for x being Element of (ClOpers L) holds S

take f ; :: thesis: for c being closure Function of L,L holds f . c = Image c

let c be closure Function of L,L; :: thesis: f . c = Image c

c is Element of (ClOpers L) by Th10;

then ex c1 being closure Function of L,L st

( c1 = c & f . c = Image c1 ) by A2;

hence f . c = Image c ; :: thesis: verum