let L1, L2 be non empty up-complete Poset; :: thesis: for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds f .: (waybelow x) = waybelow (f . x)
let f be Function of L1,L2; :: thesis: ( f is isomorphic implies for x being Element of L1 holds f .: (waybelow x) = waybelow (f . x) )
assume A1: f is isomorphic ; :: thesis: for x being Element of L1 holds f .: (waybelow x) = waybelow (f . x)
then reconsider g = f " as Function of L2,L1 by WAYBEL_0:67;
let x be Element of L1; :: thesis: f .: (waybelow x) = waybelow (f . x)
A2: waybelow (f . x) c= f .: (waybelow x)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in waybelow (f . x) or z in f .: (waybelow x) )
assume z in waybelow (f . x) ; :: thesis: z in f .: (waybelow x)
then z in { y where y is Element of L2 : y << f . x } by WAYBEL_3:def 3;
then consider z1 being Element of L2 such that
A3: z1 = z and
A4: z1 << f . x ;
g . z1 in the carrier of L1 ;
then A5: g . z1 in dom f by FUNCT_2:def 1;
z1 in the carrier of L2 ;
then z1 in dom g by FUNCT_2:def 1;
then z1 in rng f by A1, FUNCT_1:33;
then A6: z1 = f . (g . z1) by A1, FUNCT_1:35;
then g . z1 << x by A1, A4, WAYBEL13:27;
then g . z1 in waybelow x by WAYBEL_3:7;
hence z in f .: (waybelow x) by A3, A5, A6, FUNCT_1:def 6; :: thesis: verum

end;

f .: (waybelow x) c= waybelow (f . x)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f .: (waybelow x) or z in waybelow (f . x) )
assume z in f .: (waybelow x) ; :: thesis: z in waybelow (f . x)
then consider v being object such that
v in dom f and
A7: v in waybelow x and
A8: z = f . v by FUNCT_1:def 6;
v in { y where y is Element of L1 : y << x } by A7, WAYBEL_3:def 3;
then consider v1 being Element of L1 such that
A9: v1 = v and
A10: v1 << x ;
f . v1 << f . x by A1, A10, WAYBEL13:27;
hence z in waybelow (f . x) by A8, A9, WAYBEL_3:7; :: thesis: verum

end;

hence f .: (waybelow x) = waybelow (f . x) by A2, XBOOLE_0:def 10; :: thesis: verum