let A be partial non-empty UAStr ; :: thesis: for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds
( R |^ A is total & R |^ A is symmetric & R |^ A is transitive )
let R be Equivalence_Relation of the carrier of A; :: thesis: ( R c= DomRel A implies ( R |^ A is total & R |^ A is symmetric & R |^ A is transitive ) )
assume A1: R c= DomRel A ; :: thesis: ( R |^ A is total & R |^ A is symmetric & R |^ A is transitive )
now :: thesis: for x being object st x in the carrier of A holds
[x,x] in R |^ A
let x be object ; :: thesis: ( x in the carrier of A implies [x,x] in R |^ A )
assume x in the carrier of A ; :: thesis: [x,x] in R |^ A
then reconsider a = x as Element of A ;
A2: [a,a] in R by EQREL_1:5;
now :: thesis: for f being operation of A
for p, q being FinSequence st (p ^ <*a*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f holds
[(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
let f be operation of A; :: thesis: for p, q being FinSequence st (p ^ <*a*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f holds
[(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
let p, q be FinSequence; :: thesis: ( (p ^ <*a*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f implies [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R )
assume that
A3: (p ^ <*a*>) ^ q in dom f and
(p ^ <*a*>) ^ q in dom f ; :: thesis: [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
f . ((p ^ <*a*>) ^ q) in rng f by A3, FUNCT_1:def 3;
hence [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R by EQREL_1:5; :: thesis: verum
end;
hence [x,x] in R |^ A by A2, Def5; :: thesis: verum
end;
then A4: R |^ A is_reflexive_in the carrier of A ;
then A5: dom (R |^ A) = the carrier of A by ORDERS_1:13;
A6: field (R |^ A) = the carrier of A by A4, ORDERS_1:13;
thus R |^ A is total by A5, PARTFUN1:def 2; :: thesis: ( R |^ A is symmetric & R |^ A is transitive )
now :: thesis: for x, y being object st x in the carrier of A & y in the carrier of A & [x,y] in R |^ A holds
[y,x] in R |^ A
let x, y be object ; :: thesis: ( x in the carrier of A & y in the carrier of A & [x,y] in R |^ A implies [y,x] in R |^ A )
assume that
A7: x in the carrier of A and
A8: y in the carrier of A ; :: thesis: ( [x,y] in R |^ A implies [y,x] in R |^ A )
reconsider a = x, b = y as Element of A by A7, A8;
assume A9: [x,y] in R |^ A ; :: thesis: [y,x] in R |^ A
then A10: [a,b] in R by Def5;
now :: thesis: ( [b,a] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*b*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f holds
[(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R ) )
thus [b,a] in R by A10, EQREL_1:6; :: thesis: for f being operation of A
for p, q being FinSequence st (p ^ <*b*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f holds
[(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
let f be operation of A; :: thesis: for p, q being FinSequence st (p ^ <*b*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f holds
[(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
let p, q be FinSequence; :: thesis: ( (p ^ <*b*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f implies [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R )
assume that
A11: (p ^ <*b*>) ^ q in dom f and
A12: (p ^ <*a*>) ^ q in dom f ; :: thesis: [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
[(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*b*>) ^ q))] in R by A9, A11, A12, Def5;
hence [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R by EQREL_1:6; :: thesis: verum
end;
hence [y,x] in R |^ A by Def5; :: thesis: verum
end;
then R |^ A is_symmetric_in the carrier of A ;
hence R |^ A is symmetric by A6; :: thesis: R |^ A is transitive
now :: thesis: for x, y, z being object st x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in R |^ A & [y,z] in R |^ A holds
[x,z] in R |^ A
let x, y, z be object ; :: thesis: ( x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in R |^ A & [y,z] in R |^ A implies [x,z] in R |^ A )
assume that
A13: x in the carrier of A and
A14: y in the carrier of A and
A15: z in the carrier of A ; :: thesis: ( [x,y] in R |^ A & [y,z] in R |^ A implies [x,z] in R |^ A )
reconsider a = x, b = y, c = z as Element of A by A13, A14, A15;
assume that
A16: [x,y] in R |^ A and
A17: [y,z] in R |^ A ; :: thesis: [x,z] in R |^ A
A18: now :: thesis: for f being operation of A
for p, q being FinSequence st (p ^ <*a*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f holds
[(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R
let f be operation of A; :: thesis: for p, q being FinSequence st (p ^ <*a*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f holds
[(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R
let p, q be FinSequence; :: thesis: ( (p ^ <*a*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f implies [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R )
A19: [a,b] in R by A16, Def5;
A20: ( (p ^ <*a*>) ^ q in dom f & (p ^ <*b*>) ^ q in dom f implies [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*b*>) ^ q))] in R ) by A16, Def5;
( (p ^ <*b*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f implies [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R ) by A17, Def5;
hence ( (p ^ <*a*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f implies [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R ) by A1, A19, A20, Def4, EQREL_1:7; :: thesis: verum
end;
A21: [a,b] in R by A16, Def5;
[b,c] in R by A17, Def5;
then [a,c] in R by A21, EQREL_1:7;
hence [x,z] in R |^ A by A18, Def5; :: thesis: verum
end;
then R |^ A is_transitive_in the carrier of A ;
hence R |^ A is transitive by A6; :: thesis: verum