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} ;
A8: dom (id (dom f)) = dom f ;
A9: rng (id (dom f)) = dom ((id (dom f)) ") by FUNCT_1:33
.= dom f by A8, FUNCT_1:45 ;
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 A7, FUNCT_4:def 1
.= ((dom f) \/ {n}) \/ {m}
.= (dom f) \/ {m} by A4, ZFMISC_1:40
.= dom f by A3, ZFMISC_1:40 ;
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 A10, FUNCT_1:13;
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 A13, FUNCT_4:89
.= x by A14, FUNCT_4:90 ;
:: 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 A13, FUNCT_4:90
.= x by A16, FUNCT_4:89 ;
:: 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:91
.= (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x by A12, FUNCT_1:17
.= (id (dom f)) . x by A15, A17, FUNCT_4:91
.= x by A12, FUNCT_1:17 ;
:: 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 A3, ZFMISC_1:40;
then A18: (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by FUNCT_4:17, XBOOLE_1:9;
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 A4, A10, ZFMISC_1:40;
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:27, 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:17;
then A23: ((id (dom f)) +* (n .--> m)) +* (m .--> n) is one-to-one by A10, FUNCT_1:31;
rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by A18, A20;
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:40;
then A25: dom (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A5, A10, RELAT_1:27;
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 A25, FUNCT_1:12;
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 A1, A27, FUNCT_4:89; :: 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 A2, A27, FUNCT_4:90; :: 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:91
.= g . x by A26, FUNCT_1:17
.= 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:2;
rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A9, A22, A11, FUNCT_1:17;
then rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = dom g by A5, A10, A24, A19;
hence f,g are_fiberwise_equipotent by A10, A23, A30, CLASSES1:77; :: thesis: verum