let f, g be Function; :: thesis: for m, n being set st f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) holds
f,g are_fiberwise_equipotent
let m, n be set ; :: thesis: ( f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) implies f,g are_fiberwise_equipotent )
assume that
A1: f . m = g . n and
A2: f . n = g . m and
A3: m in dom f and
A4: n in dom f and
A5: dom f = dom g and
A6: for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ; :: thesis: f,g are_fiberwise_equipotent
set t = id (dom f);
set nm = n .--> m;
set mn = m .--> n;
set p = ((id (dom f)) +* (n .--> m)) +* (m .--> n);
A7: dom (n .--> m) = {n} by FUNCOP_1:19;
A8: dom (id (dom f)) = dom f by FUNCT_1:34;
A9: rng (id (dom f)) = dom ((id (dom f)) " ) by FUNCT_1:55
.= dom f by A8, FUNCT_1:67 ;
dom (m .--> n) = {m} by FUNCOP_1:19;
then A10: dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = (dom ((id (dom f)) +* (n .--> m))) \/ {m} by FUNCT_4:def 1
.= ((dom (id (dom f))) \/ {n}) \/ {m} by A7, FUNCT_4:def 1
.= ((dom f) \/ {n}) \/ {m} by FUNCT_1:34
.= (dom f) \/ {m} by A4, ZFMISC_1:46
.= dom f by A3, ZFMISC_1:46 ;

A11: now

let x be set ; :: thesis: ( x in dom f implies ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = b₁ )
assume A12: x in dom f ; :: thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = b₁
then A13: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x) by A10, FUNCT_1:23;

per cases ( x = m or x <> m ) ;

suppose A14: x = m ; :: thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = b₁

hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . n by A13, FUNCT_4:95
.= x by A14, FUNCT_4:96 ;
:: thesis: verum

end;

suppose A15: x <> m ; :: thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = b₁

now

per cases ( x = n or x <> n ) ;

suppose A16: x = n ; :: thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x

hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . m by A13, FUNCT_4:96
.= x by A16, FUNCT_4:95 ;
:: thesis: verum

end;

suppose A17: x <> n ; :: thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x

hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . ((id (dom f)) . x) by A13, A15, FUNCT_4:97
.= (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x by A12, FUNCT_1:34
.= (id (dom f)) . x by A15, A17, FUNCT_4:97
.= x by A12, FUNCT_1:34 ;
:: thesis: verum

end;

end;

end;

hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x ; :: thesis: verum

end;

end;

end;

rng (n .--> m) = {m} by FUNCOP_1:14;
then (rng (id (dom f))) \/ (rng (n .--> m)) = dom f by A3, A9, ZFMISC_1:46;
then A18: (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by FUNCT_4:18, XBOOLE_1:9;
for z being set st z in rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) holds
z in rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by FUNCT_1:25;
then A19: rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) c= rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by TARSKI:def 3;
A20: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) by FUNCT_4:18;
A21: rng (m .--> n) = {n} by FUNCOP_1:14;
then (dom f) \/ (rng (m .--> n)) = dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A4, A10, ZFMISC_1:46;
then A22: dom ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A10, A18, A20, RELAT_1:46, XBOOLE_1:1;
then (((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = id (dom f) by A11, FUNCT_1:34;
then A23: ((id (dom f)) +* (n .--> m)) +* (m .--> n) is one-to-one by A10, FUNCT_1:53;
rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by A18, A20, XBOOLE_1:1;
then A24: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A4, A10, A21, ZFMISC_1:46;
then A25: dom (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A5, A10, RELAT_1:46;

now

let x be set ; :: thesis: ( x in dom f implies (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = f . b₁ )
assume A26: x in dom f ; :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = f . b₁
then A27: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = g . ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x) by A25, FUNCT_1:22;

per cases ( x = m or x <> m ) ;

suppose x = m ; :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = f . b₁

hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x by A1, A27, FUNCT_4:95; :: thesis: verum

end;

suppose A28: x <> m ; :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = f . b₁

now

per cases ( x = n or x <> n ) ;

suppose x = n ; :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x

hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x by A2, A27, FUNCT_4:96; :: thesis: verum

end;

suppose A29: x <> n ; :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x

hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = g . ((id (dom f)) . x) by A27, A28, FUNCT_4:97
.= g . x by A26, FUNCT_1:34
.= f . x by A6, A26, A28, A29 ;
:: thesis: verum

end;

end;

end;

hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x ; :: thesis: verum

end;

end;

end;

then A30: f = g * (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A25, FUNCT_1:9;
rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A9, A22, A11, FUNCT_1:34;
then rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = dom g by A5, A10, A24, A19, XBOOLE_0:def 10;
hence f,g are_fiberwise_equipotent by A10, A23, A30, CLASSES1:85; :: thesis: verum