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 (m .--> n) = {m} by FUNCOP_1:19;
A8: dom (n .--> m) = {n} by FUNCOP_1:19;
A9: dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = (dom ((id (dom f)) +* (n .--> m))) \/ {m} by A7, FUNCT_4:def 1
.= ((dom (id (dom f))) \/ {n}) \/ {m} by A8, 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 ;
A10: dom (id (dom f)) = dom f by FUNCT_1:34;
A11: rng (n .--> m) = {m} by FUNCOP_1:14;
A12: rng (id (dom f)) = dom ((id (dom f)) " ) by FUNCT_1:55
.= dom f by A10, FUNCT_1:67 ;
then (rng (id (dom f))) \/ (rng (n .--> m)) = dom f by A3, A11, ZFMISC_1:46;
then A13: (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by FUNCT_4:18, XBOOLE_1:9;
A14: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) by FUNCT_4:18;
then A15: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by A13, XBOOLE_1:1;
A16: rng (m .--> n) = {n} by FUNCOP_1:14;
then A17: (dom f) \/ (rng (m .--> n)) = dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A4, A9, ZFMISC_1:46;
A18: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A4, A9, A15, A16, ZFMISC_1:46;
A19: dom ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A9, A13, A14, A17, RELAT_1:46, XBOOLE_1:1;

A20: 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 A21: x in dom f ; :: thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = b₁
then A22: ((((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 A9, FUNCT_1:23;

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

suppose A23: 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 A22, FUNCT_4:95
.= x by A23, FUNCT_4:96 ;
:: thesis: verum

end;

suppose A24: 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 A25: 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 A22, FUNCT_4:96
.= x by A25, FUNCT_4:95 ;
:: thesis: verum

end;

suppose A26: 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 A22, A24, FUNCT_4:97
.= (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x by A21, FUNCT_1:34
.= (id (dom f)) . x by A24, A26, FUNCT_4:97
.= x by A21, 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;

then A27: (((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = id (dom f) by A19, FUNCT_1:34;
A28: rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A12, A19, A20, FUNCT_1:34;
A29: ((id (dom f)) +* (n .--> m)) +* (m .--> n) is one-to-one by A9, A27, FUNCT_1:53;
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 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;
then A30: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = dom g by A5, A9, A18, A28, XBOOLE_0:def 10;
A31: dom (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A5, A9, A18, 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 A32: x in dom f ; :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b₁ = f . b₁
then A33: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = g . ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x) by A31, 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, A33, FUNCT_4:95; :: thesis: verum

end;

suppose A34: 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, A33, FUNCT_4:96; :: thesis: verum

end;

suppose A35: 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 A33, A34, FUNCT_4:97
.= g . x by A32, FUNCT_1:34
.= f . x by A6, A32, A34, A35 ;
:: thesis: verum

end;

end;

end;

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

end;

end;

end;

then f = g * (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A31, FUNCT_1:9;
hence f,g are_fiberwise_equipotent by A9, A29, A30, CLASSES1:85; :: thesis: verum