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:
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} ;
A8: dom (id (dom f)) = dom f ;
A9: rng (id (dom f)) = dom ((id (dom f)) ") by FUNCT_1:33
.= dom f by ;
dom (m .--> n) = {m} ;
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
.= ((dom f) \/ {n}) \/ {m}
.= (dom f) \/ {m} by
.= dom f by ;
A11: now :: thesis: for x being object st x in dom f holds
((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x
let x be object ; :: thesis: ( x in dom f implies ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1 )
assume A12: x in dom f ; :: thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1
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 ;
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))) . b1 = b1
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
.= x by ;
:: thesis: verum
end;
suppose A15: x <> m ; :: thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1
now :: thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x
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
.= x by ;
:: 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
.= (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x by
.= (id (dom f)) . x by
.= x by ;
:: 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:8;
then (rng (id (dom f))) \/ (rng (n .--> m)) = dom f by ;
then A18: (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by ;
for z being object 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:14;
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)) ;
A20: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) by FUNCT_4:17;
A21: rng (m .--> n) = {n} by FUNCOP_1:8;
then (dom f) \/ (rng (m .--> n)) = dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by ;
then A22: dom ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by ;
then (((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = id (dom f) by ;
then A23: ((id (dom f)) +* (n .--> m)) +* (m .--> n) is one-to-one by ;
rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by ;
then A24: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by ;
then A25: dom (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by ;
now :: thesis: for x being object st x in dom f holds
(g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x
let x be object ; :: thesis: ( x in dom f implies (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1 )
assume A26: x in dom f ; :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1
then A27: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = g . ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x) by ;
per cases ( x = m or x <> m ) ;
suppose x = m ; :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1
hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x by ; :: thesis: verum
end;
suppose A28: x <> m ; :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1
now :: thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x
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 ; :: 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
.= g . x by
.= 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 ;
rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by ;
then rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = dom g by A5, A10, A24, A19;
hence f,g are_fiberwise_equipotent by ; :: thesis: verum