defpred S1[ set , set ] means f . $1 = f . $2;
set u1 = the carrier of U1;
consider R being Relation of the carrier of U1, the carrier of U1 such that
A2:
for x, y being Element of the carrier of U1 holds
( [x,y] in R iff S1[x,y] )
from RELSET_1:sch 2();
R is_reflexive_in the carrier of U1
then A3:
( dom R = the carrier of U1 & field R = the carrier of U1 )
by ORDERS_1:13;
A4:
R is_transitive_in the carrier of U1
proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( not x in the carrier of U1 or not y in the carrier of U1 or not z in the carrier of U1 or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that A5:
(
x in the
carrier of
U1 &
y in the
carrier of
U1 &
z in the
carrier of
U1 )
and A6:
(
[x,y] in R &
[y,z] in R )
;
[x,z] in R
reconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of the
carrier of
U1 by A5;
(
f . x1 = f . y1 &
f . y1 = f . z1 )
by A2, A6;
hence
[x,z] in R
by A2;
verum
end;
R is_symmetric_in the carrier of U1
then reconsider R = R as Equivalence_Relation of U1 by A3, A4, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
now for n being Nat
for o being operation of U1 st n in dom the charact of U1 & o = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R
U1,
U2 are_similar
by A1;
then A9:
signature U1 = signature U2
;
let n be
Nat;
for o being operation of U1 st n in dom the charact of U1 & o = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in Rlet o be
operation of
U1;
( n in dom the charact of U1 & o = the charact of U1 . n implies for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R )assume that A10:
n in dom the
charact of
U1
and A11:
o = the
charact of
U1 . n
;
for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R
(
len (signature U1) = len the
charact of
U1 &
len (signature U2) = len the
charact of
U2 )
by UNIALG_1:def 4;
then
dom the
charact of
U2 = dom the
charact of
U1
by A9, FINSEQ_3:29;
then reconsider o2 = the
charact of
U2 . n as
operation of
U2 by A10, FUNCT_1:def 3;
let x,
y be
FinSequence of
U1;
( x in dom o & y in dom o & [x,y] in ExtendRel R implies [(o . x),(o . y)] in R )assume that A12:
(
x in dom o &
y in dom o )
and A13:
[x,y] in ExtendRel R
;
[(o . x),(o . y)] in R
(
o . x in rng o &
o . y in rng o )
by A12, FUNCT_1:def 3;
then reconsider ox =
o . x,
oy =
o . y as
Element of the
carrier of
U1 ;
A14:
len x = len y
by A13, FINSEQ_3:def 3;
A15:
len (f * y) = len y
by FINSEQ_3:120;
then A16:
dom (f * y) = Seg (len x)
by A14, FINSEQ_1:def 3;
A17:
len (f * x) = len x
by FINSEQ_3:120;
A18:
now for m being Nat st m in dom (f * y) holds
(f * y) . m = (f * x) . mlet m be
Nat;
( m in dom (f * y) implies (f * y) . m = (f * x) . m )assume A19:
m in dom (f * y)
;
(f * y) . m = (f * x) . mthen
m in dom y
by A14, A16, FINSEQ_1:def 3;
then A20:
y . m in rng y
by FUNCT_1:def 3;
A21:
m in dom x
by A16, A19, FINSEQ_1:def 3;
then
x . m in rng x
by FUNCT_1:def 3;
then reconsider xm =
x . m,
ym =
y . m as
Element of the
carrier of
U1 by A20;
[(x . m),(y . m)] in R
by A13, A21, FINSEQ_3:def 3;
then A22:
f . xm =
f . ym
by A2
.=
(f * y) . m
by A19, FINSEQ_3:120
;
m in dom (f * x)
by A17, A16, A19, FINSEQ_1:def 3;
hence
(f * y) . m = (f * x) . m
by A22, FINSEQ_3:120;
verum end;
(
f . (o . x) = o2 . (f * x) &
f . (o . y) = o2 . (f * y) )
by A1, A10, A11, A12;
then
f . ox = f . oy
by A14, A17, A15, A18, FINSEQ_2:9;
hence
[(o . x),(o . y)] in R
by A2;
verum end;
then reconsider R = R as Congruence of U1 by Def7;
take
R
; for a, b being Element of U1 holds
( [a,b] in R iff f . a = f . b )
let a, b be Element of the carrier of U1; ( [a,b] in R iff f . a = f . b )
thus
( [a,b] in R implies f . a = f . b )
by A2; ( f . a = f . b implies [a,b] in R )
assume
f . a = f . b
; [a,b] in R
hence
[a,b] in R
by A2; verum