let C, C9, D be non empty set ; :: thesis: for B being Element of Fin C

for A being Element of Fin C9

for F being BinOp of D

for f being Function of C,D

for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let B be Element of Fin C; :: thesis: for A being Element of Fin C9

for F being BinOp of D

for f being Function of C,D

for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let A be Element of Fin C9; :: thesis: for F being BinOp of D

for f being Function of C,D

for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let F be BinOp of D; :: thesis: for f being Function of C,D

for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let f be Function of C,D; :: thesis: for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let g be Function of C9,D; :: thesis: ( F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) implies F $$ (A,g) = F $$ (B,f) )

defpred S_{1}[ Element of Fin C9] means ( ( $1 <> {} or F is having_a_unity ) implies for B being Element of Fin C st ex s being Function st

( dom s = $1 & rng s = B & s is one-to-one & g | $1 = f * s ) holds

F $$ ($1,g) = F $$ (B,f) );

assume A1: ( F is commutative & F is associative ) ; :: thesis: ( ( not A <> {} & not F is having_a_unity ) or for s being Function holds

( not dom s = A or not rng s = B or not s is one-to-one or not g | A = f * s ) or F $$ (A,g) = F $$ (B,f) )

A2: for B9 being Element of Fin C9

for b being Element of C9 st S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {.b.}]
_{1}[ {}. C9]
_{1}[A]
from SETWISEO:sch 2(A61, A2);

hence ( ( not A <> {} & not F is having_a_unity ) or for s being Function holds

( not dom s = A or not rng s = B or not s is one-to-one or not g | A = f * s ) or F $$ (A,g) = F $$ (B,f) ) ; :: thesis: verum

for A being Element of Fin C9

for F being BinOp of D

for f being Function of C,D

for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let B be Element of Fin C; :: thesis: for A being Element of Fin C9

for F being BinOp of D

for f being Function of C,D

for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let A be Element of Fin C9; :: thesis: for F being BinOp of D

for f being Function of C,D

for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let F be BinOp of D; :: thesis: for f being Function of C,D

for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let f be Function of C,D; :: thesis: for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds

F $$ (A,g) = F $$ (B,f)

let g be Function of C9,D; :: thesis: ( F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st

( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) implies F $$ (A,g) = F $$ (B,f) )

defpred S

( dom s = $1 & rng s = B & s is one-to-one & g | $1 = f * s ) holds

F $$ ($1,g) = F $$ (B,f) );

assume A1: ( F is commutative & F is associative ) ; :: thesis: ( ( not A <> {} & not F is having_a_unity ) or for s being Function holds

( not dom s = A or not rng s = B or not s is one-to-one or not g | A = f * s ) or F $$ (A,g) = F $$ (B,f) )

A2: for B9 being Element of Fin C9

for b being Element of C9 st S

S

proof

A61:
S
let A9 be Element of Fin C9; :: thesis: for b being Element of C9 st S_{1}[A9] & not b in A9 holds

S_{1}[A9 \/ {.b.}]

let a be Element of C9; :: thesis: ( S_{1}[A9] & not a in A9 implies S_{1}[A9 \/ {.a.}] )

assume that

A3: ( ( A9 <> {} or F is having_a_unity ) implies for B being Element of Fin C st ex s being Function st

( dom s = A9 & rng s = B & s is one-to-one & g | A9 = f * s ) holds

F $$ (A9,g) = F $$ (B,f) ) and

A4: not a in A9 ; :: thesis: S_{1}[A9 \/ {.a.}]

assume ( A9 \/ {a} <> {} or F is having_a_unity ) ; :: thesis: for B being Element of Fin C st ex s being Function st

( dom s = A9 \/ {.a.} & rng s = B & s is one-to-one & g | (A9 \/ {.a.}) = f * s ) holds

F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)

let B be Element of Fin C; :: thesis: ( ex s being Function st

( dom s = A9 \/ {.a.} & rng s = B & s is one-to-one & g | (A9 \/ {.a.}) = f * s ) implies F $$ ((A9 \/ {.a.}),g) = F $$ (B,f) )

set A = A9 \/ {.a.};

given s being Function such that A5: dom s = A9 \/ {.a.} and

A6: rng s = B and

A7: s is one-to-one and

A8: g | (A9 \/ {.a.}) = f * s ; :: thesis: F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)

A9: a in A9 \/ {.a.} by ZFMISC_1:136;

then A10: s . a in B by A5, A6, FUNCT_1:def 3;

B c= C by FINSUB_1:def 5;

then reconsider c = s . a as Element of C by A10;

set B9 = B \ {.c.};

set s9 = s | A9;

A11: s | A9 is one-to-one by A7, FUNCT_1:52;

a in C9 ;

then a in dom g by FUNCT_2:def 1;

then a in (dom g) /\ (A9 \/ {.a.}) by A9, XBOOLE_0:def 4;

then ( a in dom (f * s) & g . a = (f * s) . a ) by A8, FUNCT_1:48, RELAT_1:61;

then A34: g . a = f . c by FUNCT_1:12;

(B \ {.c.}) \/ {c} = B \/ {c} by XBOOLE_1:39;

then A35: B = (B \ {.c.}) \/ {c} by A10, ZFMISC_1:40;

A36: dom (s | A9) = A9 by A5, RELAT_1:62, XBOOLE_1:7;

A37: for x being object st x in dom (g | A9) holds

(g | A9) . x = (f * (s | A9)) . x

A56: not c in B \ {.c.} by ZFMISC_1:56;

end;S

let a be Element of C9; :: thesis: ( S

assume that

A3: ( ( A9 <> {} or F is having_a_unity ) implies for B being Element of Fin C st ex s being Function st

( dom s = A9 & rng s = B & s is one-to-one & g | A9 = f * s ) holds

F $$ (A9,g) = F $$ (B,f) ) and

A4: not a in A9 ; :: thesis: S

assume ( A9 \/ {a} <> {} or F is having_a_unity ) ; :: thesis: for B being Element of Fin C st ex s being Function st

( dom s = A9 \/ {.a.} & rng s = B & s is one-to-one & g | (A9 \/ {.a.}) = f * s ) holds

F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)

let B be Element of Fin C; :: thesis: ( ex s being Function st

( dom s = A9 \/ {.a.} & rng s = B & s is one-to-one & g | (A9 \/ {.a.}) = f * s ) implies F $$ ((A9 \/ {.a.}),g) = F $$ (B,f) )

set A = A9 \/ {.a.};

given s being Function such that A5: dom s = A9 \/ {.a.} and

A6: rng s = B and

A7: s is one-to-one and

A8: g | (A9 \/ {.a.}) = f * s ; :: thesis: F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)

A9: a in A9 \/ {.a.} by ZFMISC_1:136;

then A10: s . a in B by A5, A6, FUNCT_1:def 3;

B c= C by FINSUB_1:def 5;

then reconsider c = s . a as Element of C by A10;

set B9 = B \ {.c.};

set s9 = s | A9;

A11: s | A9 is one-to-one by A7, FUNCT_1:52;

now :: thesis: for y being object holds

( ( y in rng (s | A9) implies y in B \ {.c.} ) & ( y in B \ {.c.} implies y in rng (s | A9) ) )

then A21:
rng (s | A9) = B \ {.c.}
by TARSKI:2;( ( y in rng (s | A9) implies y in B \ {.c.} ) & ( y in B \ {.c.} implies y in rng (s | A9) ) )

let y be object ; :: thesis: ( ( y in rng (s | A9) implies y in B \ {.c.} ) & ( y in B \ {.c.} implies y in rng (s | A9) ) )

thus ( y in rng (s | A9) implies y in B \ {.c.} ) :: thesis: ( y in B \ {.c.} implies y in rng (s | A9) )

then y in B by XBOOLE_0:def 5;

then consider x being object such that

A18: x in dom s and

A19: y = s . x by A6, FUNCT_1:def 3;

A20: ( x in A9 or x in {a} ) by A5, A18, XBOOLE_0:def 3;

not y in {c} by A17, XBOOLE_0:def 5;

then x <> a by A19, TARSKI:def 1;

then x in (dom s) /\ A9 by A18, A20, TARSKI:def 1, XBOOLE_0:def 4;

then ( x in dom (s | A9) & (s | A9) . x = s . x ) by FUNCT_1:48, RELAT_1:61;

hence y in rng (s | A9) by A19, FUNCT_1:def 3; :: thesis: verum

end;thus ( y in rng (s | A9) implies y in B \ {.c.} ) :: thesis: ( y in B \ {.c.} implies y in rng (s | A9) )

proof

assume A17:
y in B \ {.c.}
; :: thesis: y in rng (s | A9)
assume
y in rng (s | A9)
; :: thesis: y in B \ {.c.}

then consider x being object such that

A12: x in dom (s | A9) and

A13: y = (s | A9) . x by FUNCT_1:def 3;

A14: (s | A9) . x = s . x by A12, FUNCT_1:47;

A15: x in (dom s) /\ A9 by A12, RELAT_1:61;

then ( x in dom s & x <> a ) by A4, XBOOLE_0:def 4;

then s . x <> c by A5, A7, A9, FUNCT_1:def 4;

then A16: not y in {c} by A13, A14, TARSKI:def 1;

x in dom s by A15, XBOOLE_0:def 4;

then y in B by A6, A13, A14, FUNCT_1:def 3;

hence y in B \ {.c.} by A16, XBOOLE_0:def 5; :: thesis: verum

end;then consider x being object such that

A12: x in dom (s | A9) and

A13: y = (s | A9) . x by FUNCT_1:def 3;

A14: (s | A9) . x = s . x by A12, FUNCT_1:47;

A15: x in (dom s) /\ A9 by A12, RELAT_1:61;

then ( x in dom s & x <> a ) by A4, XBOOLE_0:def 4;

then s . x <> c by A5, A7, A9, FUNCT_1:def 4;

then A16: not y in {c} by A13, A14, TARSKI:def 1;

x in dom s by A15, XBOOLE_0:def 4;

then y in B by A6, A13, A14, FUNCT_1:def 3;

hence y in B \ {.c.} by A16, XBOOLE_0:def 5; :: thesis: verum

then y in B by XBOOLE_0:def 5;

then consider x being object such that

A18: x in dom s and

A19: y = s . x by A6, FUNCT_1:def 3;

A20: ( x in A9 or x in {a} ) by A5, A18, XBOOLE_0:def 3;

not y in {c} by A17, XBOOLE_0:def 5;

then x <> a by A19, TARSKI:def 1;

then x in (dom s) /\ A9 by A18, A20, TARSKI:def 1, XBOOLE_0:def 4;

then ( x in dom (s | A9) & (s | A9) . x = s . x ) by FUNCT_1:48, RELAT_1:61;

hence y in rng (s | A9) by A19, FUNCT_1:def 3; :: thesis: verum

now :: thesis: for x being object holds

( ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) & ( x in dom (f * (s | A9)) implies x in dom (g | A9) ) )

then A33:
dom (g | A9) = dom (f * (s | A9))
by TARSKI:2;( ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) & ( x in dom (f * (s | A9)) implies x in dom (g | A9) ) )

let x be object ; :: thesis: ( ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) & ( x in dom (f * (s | A9)) implies x in dom (g | A9) ) )

thus ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) :: thesis: ( x in dom (f * (s | A9)) implies x in dom (g | A9) )

then A29: x in dom (s | A9) by FUNCT_1:11;

then A30: x in (dom s) /\ A9 by RELAT_1:61;

then A31: x in dom s by XBOOLE_0:def 4;

(s | A9) . x in dom f by A28, FUNCT_1:11;

then s . x in dom f by A29, FUNCT_1:47;

then x in dom (g | (A9 \/ {.a.})) by A8, A31, FUNCT_1:11;

then x in (dom g) /\ (A9 \/ {.a.}) by RELAT_1:61;

then A32: x in dom g by XBOOLE_0:def 4;

x in A9 by A30, XBOOLE_0:def 4;

then x in (dom g) /\ A9 by A32, XBOOLE_0:def 4;

hence x in dom (g | A9) by RELAT_1:61; :: thesis: verum

end;thus ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) :: thesis: ( x in dom (f * (s | A9)) implies x in dom (g | A9) )

proof

assume A28:
x in dom (f * (s | A9))
; :: thesis: x in dom (g | A9)
assume
x in dom (g | A9)
; :: thesis: x in dom (f * (s | A9))

then A22: x in (dom g) /\ A9 by RELAT_1:61;

then A23: x in A9 by XBOOLE_0:def 4;

A24: x in dom g by A22, XBOOLE_0:def 4;

x in A9 \/ {.a.} by A23, ZFMISC_1:136;

then x in (dom g) /\ (A9 \/ {.a.}) by A24, XBOOLE_0:def 4;

then A25: x in dom (f * s) by A8, RELAT_1:61;

then A26: s . x in dom f by FUNCT_1:11;

x in dom s by A25, FUNCT_1:11;

then x in (dom s) /\ A9 by A23, XBOOLE_0:def 4;

then A27: x in dom (s | A9) by RELAT_1:61;

then (s | A9) . x = s . x by FUNCT_1:47;

hence x in dom (f * (s | A9)) by A26, A27, FUNCT_1:11; :: thesis: verum

end;then A22: x in (dom g) /\ A9 by RELAT_1:61;

then A23: x in A9 by XBOOLE_0:def 4;

A24: x in dom g by A22, XBOOLE_0:def 4;

x in A9 \/ {.a.} by A23, ZFMISC_1:136;

then x in (dom g) /\ (A9 \/ {.a.}) by A24, XBOOLE_0:def 4;

then A25: x in dom (f * s) by A8, RELAT_1:61;

then A26: s . x in dom f by FUNCT_1:11;

x in dom s by A25, FUNCT_1:11;

then x in (dom s) /\ A9 by A23, XBOOLE_0:def 4;

then A27: x in dom (s | A9) by RELAT_1:61;

then (s | A9) . x = s . x by FUNCT_1:47;

hence x in dom (f * (s | A9)) by A26, A27, FUNCT_1:11; :: thesis: verum

then A29: x in dom (s | A9) by FUNCT_1:11;

then A30: x in (dom s) /\ A9 by RELAT_1:61;

then A31: x in dom s by XBOOLE_0:def 4;

(s | A9) . x in dom f by A28, FUNCT_1:11;

then s . x in dom f by A29, FUNCT_1:47;

then x in dom (g | (A9 \/ {.a.})) by A8, A31, FUNCT_1:11;

then x in (dom g) /\ (A9 \/ {.a.}) by RELAT_1:61;

then A32: x in dom g by XBOOLE_0:def 4;

x in A9 by A30, XBOOLE_0:def 4;

then x in (dom g) /\ A9 by A32, XBOOLE_0:def 4;

hence x in dom (g | A9) by RELAT_1:61; :: thesis: verum

a in C9 ;

then a in dom g by FUNCT_2:def 1;

then a in (dom g) /\ (A9 \/ {.a.}) by A9, XBOOLE_0:def 4;

then ( a in dom (f * s) & g . a = (f * s) . a ) by A8, FUNCT_1:48, RELAT_1:61;

then A34: g . a = f . c by FUNCT_1:12;

(B \ {.c.}) \/ {c} = B \/ {c} by XBOOLE_1:39;

then A35: B = (B \ {.c.}) \/ {c} by A10, ZFMISC_1:40;

A36: dom (s | A9) = A9 by A5, RELAT_1:62, XBOOLE_1:7;

A37: for x being object st x in dom (g | A9) holds

(g | A9) . x = (f * (s | A9)) . x

proof

then A44:
g | A9 = f * (s | A9)
by A33, FUNCT_1:2;
let x be object ; :: thesis: ( x in dom (g | A9) implies (g | A9) . x = (f * (s | A9)) . x )

assume x in dom (g | A9) ; :: thesis: (g | A9) . x = (f * (s | A9)) . x

then A38: x in (dom g) /\ A9 by RELAT_1:61;

then A39: x in A9 by XBOOLE_0:def 4;

then A40: x in A9 \/ {.a.} by ZFMISC_1:136;

x in dom g by A38, XBOOLE_0:def 4;

then x in (dom g) /\ (A9 \/ {.a.}) by A40, XBOOLE_0:def 4;

then x in dom (f * s) by A8, RELAT_1:61;

then A41: x in dom s by FUNCT_1:11;

then x in (dom s) /\ A9 by A39, XBOOLE_0:def 4;

then A42: x in dom (s | A9) by RELAT_1:61;

then A43: (s | A9) . x = s . x by FUNCT_1:47;

thus (g | A9) . x = g . x by A39, FUNCT_1:49

.= (f * s) . x by A8, A40, FUNCT_1:49

.= f . (s . x) by A41, FUNCT_1:13

.= (f * (s | A9)) . x by A42, A43, FUNCT_1:13 ; :: thesis: verum

end;assume x in dom (g | A9) ; :: thesis: (g | A9) . x = (f * (s | A9)) . x

then A38: x in (dom g) /\ A9 by RELAT_1:61;

then A39: x in A9 by XBOOLE_0:def 4;

then A40: x in A9 \/ {.a.} by ZFMISC_1:136;

x in dom g by A38, XBOOLE_0:def 4;

then x in (dom g) /\ (A9 \/ {.a.}) by A40, XBOOLE_0:def 4;

then x in dom (f * s) by A8, RELAT_1:61;

then A41: x in dom s by FUNCT_1:11;

then x in (dom s) /\ A9 by A39, XBOOLE_0:def 4;

then A42: x in dom (s | A9) by RELAT_1:61;

then A43: (s | A9) . x = s . x by FUNCT_1:47;

thus (g | A9) . x = g . x by A39, FUNCT_1:49

.= (f * s) . x by A8, A40, FUNCT_1:49

.= f . (s . x) by A41, FUNCT_1:13

.= (f * (s | A9)) . x by A42, A43, FUNCT_1:13 ; :: thesis: verum

now :: thesis: for y being object holds

( ( y in g .: A9 implies y in f .: (B \ {.c.}) ) & ( y in f .: (B \ {.c.}) implies y in g .: A9 ) )

then A55:
f .: (B \ {.c.}) = g .: A9
by TARSKI:2;( ( y in g .: A9 implies y in f .: (B \ {.c.}) ) & ( y in f .: (B \ {.c.}) implies y in g .: A9 ) )

let y be object ; :: thesis: ( ( y in g .: A9 implies y in f .: (B \ {.c.}) ) & ( y in f .: (B \ {.c.}) implies y in g .: A9 ) )

thus ( y in g .: A9 implies y in f .: (B \ {.c.}) ) :: thesis: ( y in f .: (B \ {.c.}) implies y in g .: A9 )

then consider x being object such that

x in dom f and

A51: x in B \ {.c.} and

A52: y = f . x by FUNCT_1:def 6;

set x9 = ((s | A9) ") . x;

A53: ((s | A9) ") . x in A9 by A11, A36, A21, A51, FUNCT_1:32;

A9 c= C9 by FINSUB_1:def 5;

then ((s | A9) ") . x in C9 by A53;

then A54: ((s | A9) ") . x in dom g by FUNCT_2:def 1;

(s | A9) . (((s | A9) ") . x) = x by A11, A21, A51, FUNCT_1:35;

then y = (f * (s | A9)) . (((s | A9) ") . x) by A36, A52, A53, FUNCT_1:13

.= g . (((s | A9) ") . x) by A44, A53, FUNCT_1:49 ;

hence y in g .: A9 by A53, A54, FUNCT_1:def 6; :: thesis: verum

end;thus ( y in g .: A9 implies y in f .: (B \ {.c.}) ) :: thesis: ( y in f .: (B \ {.c.}) implies y in g .: A9 )

proof

assume
y in f .: (B \ {.c.})
; :: thesis: y in g .: A9
assume
y in g .: A9
; :: thesis: y in f .: (B \ {.c.})

then consider x being object such that

A45: x in dom g and

A46: x in A9 and

A47: y = g . x by FUNCT_1:def 6;

x in (dom g) /\ A9 by A45, A46, XBOOLE_0:def 4;

then A48: x in dom (g | A9) by RELAT_1:61;

then x in dom (s | A9) by A33, FUNCT_1:11;

then A49: (s | A9) . x in B \ {.c.} by A21, FUNCT_1:def 3;

y = (f * (s | A9)) . x by A44, A46, A47, FUNCT_1:49;

then A50: y = f . ((s | A9) . x) by A33, A48, FUNCT_1:12;

(s | A9) . x in dom f by A33, A48, FUNCT_1:11;

hence y in f .: (B \ {.c.}) by A50, A49, FUNCT_1:def 6; :: thesis: verum

end;then consider x being object such that

A45: x in dom g and

A46: x in A9 and

A47: y = g . x by FUNCT_1:def 6;

x in (dom g) /\ A9 by A45, A46, XBOOLE_0:def 4;

then A48: x in dom (g | A9) by RELAT_1:61;

then x in dom (s | A9) by A33, FUNCT_1:11;

then A49: (s | A9) . x in B \ {.c.} by A21, FUNCT_1:def 3;

y = (f * (s | A9)) . x by A44, A46, A47, FUNCT_1:49;

then A50: y = f . ((s | A9) . x) by A33, A48, FUNCT_1:12;

(s | A9) . x in dom f by A33, A48, FUNCT_1:11;

hence y in f .: (B \ {.c.}) by A50, A49, FUNCT_1:def 6; :: thesis: verum

then consider x being object such that

x in dom f and

A51: x in B \ {.c.} and

A52: y = f . x by FUNCT_1:def 6;

set x9 = ((s | A9) ") . x;

A53: ((s | A9) ") . x in A9 by A11, A36, A21, A51, FUNCT_1:32;

A9 c= C9 by FINSUB_1:def 5;

then ((s | A9) ") . x in C9 by A53;

then A54: ((s | A9) ") . x in dom g by FUNCT_2:def 1;

(s | A9) . (((s | A9) ") . x) = x by A11, A21, A51, FUNCT_1:35;

then y = (f * (s | A9)) . (((s | A9) ") . x) by A36, A52, A53, FUNCT_1:13

.= g . (((s | A9) ") . x) by A44, A53, FUNCT_1:49 ;

hence y in g .: A9 by A53, A54, FUNCT_1:def 6; :: thesis: verum

A56: not c in B \ {.c.} by ZFMISC_1:56;

now :: thesis: F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)end;

hence
F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)
; :: thesis: verumper cases
( A9 = {} or A9 <> {} )
;

end;

suppose A57:
A9 = {}
; :: thesis: F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)

B \ {.c.} c= C
by FINSUB_1:def 5;

then B \ {.c.} c= dom f by FUNCT_2:def 1;

then A58: B \ {.c.} = {} by A55, A57;

thus F $$ ((A9 \/ {.a.}),g) = f . c by A1, A34, A57, SETWISEO:17

.= F $$ (B,f) by A1, A35, A58, SETWISEO:17 ; :: thesis: verum

end;then B \ {.c.} c= dom f by FUNCT_2:def 1;

then A58: B \ {.c.} = {} by A55, A57;

thus F $$ ((A9 \/ {.a.}),g) = f . c by A1, A34, A57, SETWISEO:17

.= F $$ (B,f) by A1, A35, A58, SETWISEO:17 ; :: thesis: verum

suppose A59:
A9 <> {}
; :: thesis: F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)

A9 c= C9
by FINSUB_1:def 5;

then A9 c= dom g by FUNCT_2:def 1;

then A60: B \ {.c.} <> {} by A55, A59;

thus F $$ ((A9 \/ {.a.}),g) = F . ((F $$ (A9,g)),(g . a)) by A1, A4, A59, Th2

.= F . ((F $$ ((B \ {.c.}),f)),(f . c)) by A3, A34, A11, A36, A21, A33, A37, A59, FUNCT_1:2

.= F $$ (B,f) by A1, A35, A56, A60, Th2 ; :: thesis: verum

end;then A9 c= dom g by FUNCT_2:def 1;

then A60: B \ {.c.} <> {} by A55, A59;

thus F $$ ((A9 \/ {.a.}),g) = F . ((F $$ (A9,g)),(g . a)) by A1, A4, A59, Th2

.= F . ((F $$ ((B \ {.c.}),f)),(f . c)) by A3, A34, A11, A36, A21, A33, A37, A59, FUNCT_1:2

.= F $$ (B,f) by A1, A35, A56, A60, Th2 ; :: thesis: verum

proof

for A being Element of Fin C9 holds S
assume A62:
( {}. C9 <> {} or F is having_a_unity )
; :: thesis: for B being Element of Fin C st ex s being Function st

( dom s = {}. C9 & rng s = B & s is one-to-one & g | ({}. C9) = f * s ) holds

F $$ (({}. C9),g) = F $$ (B,f)

let B be Element of Fin C; :: thesis: ( ex s being Function st

( dom s = {}. C9 & rng s = B & s is one-to-one & g | ({}. C9) = f * s ) implies F $$ (({}. C9),g) = F $$ (B,f) )

given s being Function such that A63: ( dom s = {}. C9 & rng s = B & s is one-to-one ) and

g | ({}. C9) = f * s ; :: thesis: F $$ (({}. C9),g) = F $$ (B,f)

B, {} are_equipotent by A63, WELLORD2:def 4;

then A64: B = {}. C by CARD_1:26;

F $$ (({}. C9),g) = the_unity_wrt F by A1, A62, SETWISEO:31;

hence F $$ (({}. C9),g) = F $$ (B,f) by A1, A62, A64, SETWISEO:31; :: thesis: verum

end;( dom s = {}. C9 & rng s = B & s is one-to-one & g | ({}. C9) = f * s ) holds

F $$ (({}. C9),g) = F $$ (B,f)

let B be Element of Fin C; :: thesis: ( ex s being Function st

( dom s = {}. C9 & rng s = B & s is one-to-one & g | ({}. C9) = f * s ) implies F $$ (({}. C9),g) = F $$ (B,f) )

given s being Function such that A63: ( dom s = {}. C9 & rng s = B & s is one-to-one ) and

g | ({}. C9) = f * s ; :: thesis: F $$ (({}. C9),g) = F $$ (B,f)

B, {} are_equipotent by A63, WELLORD2:def 4;

then A64: B = {}. C by CARD_1:26;

F $$ (({}. C9),g) = the_unity_wrt F by A1, A62, SETWISEO:31;

hence F $$ (({}. C9),g) = F $$ (B,f) by A1, A62, A64, SETWISEO:31; :: thesis: verum

hence ( ( not A <> {} & not F is having_a_unity ) or for s being Function holds

( not dom s = A or not rng s = B or not s is one-to-one or not g | A = f * s ) or F $$ (A,g) = F $$ (B,f) ) ; :: thesis: verum