set u1 = the carrier of U1;
defpred S1[ set , set ] means f . $1 = f . $2;
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:98;
A4:
R is_symmetric_in the carrier of U1
R is_transitive_in the carrier of U1
proof
let x,
y,
z be
set ;
:: according to RELAT_2:def 8 :: thesis: ( 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 A6:
(
x in the
carrier of
U1 &
y in the
carrier of
U1 &
z in the
carrier of
U1 &
[x,y] in R &
[y,z] in R )
;
:: thesis: [x,z] in R
then reconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of the
carrier of
U1 ;
(
f . x1 = f . y1 &
f . y1 = f . z1 )
by A2, A6;
hence
[x,z] in R
by A2;
:: thesis: verum
end;
then reconsider R = R as Equivalence_Relation of U1 by A3, A4, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16;
now let n be
Element of
NAT ;
:: thesis: 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;
:: thesis: ( 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 A7:
(
n in dom the
charact of
U1 &
o = the
charact of
U1 . n )
;
:: thesis: 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 x,
y be
FinSequence of
U1;
:: thesis: ( x in dom o & y in dom o & [x,y] in ExtendRel R implies [(o . x),(o . y)] in R )assume A8:
(
x in dom o &
y in dom o &
[x,y] in ExtendRel R )
;
:: thesis: [(o . x),(o . y)] in Rthen A9:
(
len x = len y & ( for
m being
Element of
NAT st
m in dom x holds
[(x . m),(y . m)] in R ) )
by Def9;
(
rng o c= the
carrier of
U1 &
o . x in rng o &
o . y in rng o )
by A8, FUNCT_1:def 5;
then reconsider ox =
o . x,
oy =
o . y as
Element of the
carrier of
U1 ;
A10:
(
U1,
U2 are_similar &
len (signature U1) = len the
charact of
U1 &
len (signature U2) = len the
charact of
U2 )
by A1, Def1, UNIALG_1:def 11;
then
signature U1 = signature U2
by UNIALG_2:def 2;
then
dom the
charact of
U2 = dom the
charact of
U1
by A10, FINSEQ_3:31;
then reconsider o2 = the
charact of
U2 . n as
operation of
U2 by A7, FUNCT_1:def 5;
A11:
(
f . (o . x) = o2 . (f * x) &
f . (o . y) = o2 . (f * y) )
by A1, A7, A8, Def1;
A12:
(
len (f * x) = len x &
len (f * y) = len y )
by Th1;
then X:
dom (f * y) = Seg (len x)
by FINSEQ_1:def 3, A9;
now let m be
Nat;
:: thesis: ( m in dom (f * y) implies (f * y) . m = (f * x) . m )assume Z:
m in dom (f * y)
;
:: thesis: (f * y) . m = (f * x) . mthen A13:
(
m in dom x &
m in dom y &
m in dom (f * x) &
m in dom (f * y) )
by A9, A12, FINSEQ_1:def 3, X;
then A14:
[(x . m),(y . m)] in R
by A8, Def9;
(
rng x c= the
carrier of
U1 &
rng y c= the
carrier of
U1 &
x . m in rng x &
y . m in rng y )
by A13, FUNCT_1:def 5;
then reconsider xm =
x . m,
ym =
y . m as
Element of the
carrier of
U1 ;
f . xm =
f . ym
by A2, A14
.=
(f * y) . m
by Z, Th1
;
hence
(f * y) . m = (f * x) . m
by A13, Th1;
:: thesis: verum end; then
f . ox = f . oy
by A9, A11, A12, FINSEQ_2:10;
hence
[(o . x),(o . y)] in R
by A2;
:: thesis: verum end;
then reconsider R = R as Congruence of U1 by Def10;
take
R
; :: thesis: 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; :: thesis: ( [a,b] in R iff f . a = f . b )
thus
( [a,b] in R implies f . a = f . b )
by A2; :: thesis: ( f . a = f . b implies [a,b] in R )
assume
f . a = f . b
; :: thesis: [a,b] in R
hence
[a,b] in R
by A2; :: thesis: verum