let C, D be non empty set ; :: thesis: for f being one-to-one PartFunc of C,D

for g being PartFunc of D,C holds

( g = f " iff ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )

let f be one-to-one PartFunc of C,D; :: thesis: for g being PartFunc of D,C holds

( g = f " iff ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )

let g be PartFunc of D,C; :: thesis: ( g = f " iff ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )

thus ( g = f " implies ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) ) :: thesis: ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) implies g = f " )

A7: dom g = rng f and

A8: for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) and

A9: g <> f " ; :: thesis: contradiction

for g being PartFunc of D,C holds

( g = f " iff ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )

let f be one-to-one PartFunc of C,D; :: thesis: for g being PartFunc of D,C holds

( g = f " iff ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )

let g be PartFunc of D,C; :: thesis: ( g = f " iff ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )

thus ( g = f " implies ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) ) :: thesis: ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) implies g = f " )

proof

assume that
assume A1:
g = f "
; :: thesis: ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) )

hence dom g = rng f by FUNCT_1:32; :: thesis: for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )

let d be Element of D; :: thesis: for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )

let c be Element of C; :: thesis: ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )

A2: dom g = rng f by A1, FUNCT_1:32;

thus ( d in rng f & c = g /. d implies ( c in dom f & d = f /. c ) ) :: thesis: ( c in dom f & d = f /. c implies ( d in rng f & c = g /. d ) )

A5: c in dom f and

A6: d = f /. c ; :: thesis: ( d in rng f & c = g /. d )

d = f . c by A5, A6, PARTFUN1:def 6;

then ( d in rng f & c = g . d ) by A1, A5, FUNCT_1:32;

hence ( d in rng f & c = g /. d ) by A2, PARTFUN1:def 6; :: thesis: verum

end;for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) )

hence dom g = rng f by FUNCT_1:32; :: thesis: for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )

let d be Element of D; :: thesis: for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )

let c be Element of C; :: thesis: ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )

A2: dom g = rng f by A1, FUNCT_1:32;

thus ( d in rng f & c = g /. d implies ( c in dom f & d = f /. c ) ) :: thesis: ( c in dom f & d = f /. c implies ( d in rng f & c = g /. d ) )

proof

assume that
assume that

A3: d in rng f and

A4: c = g /. d ; :: thesis: ( c in dom f & d = f /. c )

c = g . d by A2, A3, A4, PARTFUN1:def 6;

then ( c in dom f & d = f . c ) by A1, A3, FUNCT_1:32;

hence ( c in dom f & d = f /. c ) by PARTFUN1:def 6; :: thesis: verum

end;A3: d in rng f and

A4: c = g /. d ; :: thesis: ( c in dom f & d = f /. c )

c = g . d by A2, A3, A4, PARTFUN1:def 6;

then ( c in dom f & d = f . c ) by A1, A3, FUNCT_1:32;

hence ( c in dom f & d = f /. c ) by PARTFUN1:def 6; :: thesis: verum

A5: c in dom f and

A6: d = f /. c ; :: thesis: ( d in rng f & c = g /. d )

d = f . c by A5, A6, PARTFUN1:def 6;

then ( d in rng f & c = g . d ) by A1, A5, FUNCT_1:32;

hence ( d in rng f & c = g /. d ) by A2, PARTFUN1:def 6; :: thesis: verum

A7: dom g = rng f and

A8: for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) and

A9: g <> f " ; :: thesis: contradiction

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( dom (f ") <> dom g or ex d being Element of D st

( d in dom (f ") & (f ") /. d <> g /. d ) ) by A9, Th1;

end;

( d in dom (f ") & (f ") /. d <> g /. d ) ) by A9, Th1;

suppose
ex d being Element of D st

( d in dom (f ") & (f ") /. d <> g /. d ) ; :: thesis: contradiction

( d in dom (f ") & (f ") /. d <> g /. d ) ; :: thesis: contradiction

then consider d being Element of D such that

A10: d in dom (f ") and

A11: (f ") /. d <> g /. d ;

(f ") /. d in rng (f ") by A10, Th2;

then A12: (f ") /. d in dom f by FUNCT_1:33;

d in rng f by A10, FUNCT_1:33;

then d = f . ((f ") . d) by FUNCT_1:35;

then d = f . ((f ") /. d) by A10, PARTFUN1:def 6;

then d = f /. ((f ") /. d) by A12, PARTFUN1:def 6;

hence contradiction by A8, A11, A12; :: thesis: verum

end;A10: d in dom (f ") and

A11: (f ") /. d <> g /. d ;

(f ") /. d in rng (f ") by A10, Th2;

then A12: (f ") /. d in dom f by FUNCT_1:33;

d in rng f by A10, FUNCT_1:33;

then d = f . ((f ") . d) by FUNCT_1:35;

then d = f . ((f ") /. d) by A10, PARTFUN1:def 6;

then d = f /. ((f ") /. d) by A12, PARTFUN1:def 6;

hence contradiction by A8, A11, A12; :: thesis: verum