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

let x be set ; :: 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:11;

now

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 ( (p ^ <*a*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f ) ; :: thesis: [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
then ( f . ((p ^ <*a*>) ^ q) in rng f & f . ((p ^ <*a*>) ^ q) in rng f & rng f c= the carrier of A ) by FUNCT_1:def 5;
hence [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R by EQREL_1:11; :: thesis: verum

end;

hence [x,x] in R |^ A by A2, Def6; :: thesis: verum

end;

then R |^ A is_reflexive_in the carrier of A by RELAT_2:def 1;
then A3: ( dom (R |^ A) = the carrier of A & field (R |^ A) = the carrier of A ) by ORDERS_1:98;
hence R |^ A is total by PARTFUN1:def 4; :: thesis: ( R |^ A is symmetric & R |^ A is transitive )

now

let x, y be set ; :: 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 ( x in the carrier of A & y in the carrier of A ) ; :: thesis: ( [x,y] in R |^ A implies [y,x] in R |^ A )
then reconsider a = x, b = y as Element of A ;
assume A4: [x,y] in R |^ A ; :: thesis: [y,x] in R |^ A
then A5: ( [a,b] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*a*>) ^ q in dom f & (p ^ <*b*>) ^ q in dom f holds
[(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*b*>) ^ q))] in R ) ) by Def6;

now

thus [b,a] in R by A5, EQREL_1:12; :: 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 ( (p ^ <*b*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f ) ; :: thesis: [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
then [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*b*>) ^ q))] in R by A4, Def6;
hence [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R by EQREL_1:12; :: thesis: verum

end;

hence [y,x] in R |^ A by Def6; :: thesis: verum

end;

then R |^ A is_symmetric_in the carrier of A by RELAT_2:def 3;
hence R |^ A is symmetric by A3, RELAT_2:def 11; :: thesis: R |^ A is transitive

now

let x, y, z be set ; :: 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 ( x in the carrier of A & y in the carrier of A & z in the carrier of A ) ; :: thesis: ( [x,y] in R |^ A & [y,z] in R |^ A implies [x,z] in R |^ A )
then reconsider a = x, b = y, c = z as Element of A ;
assume A6: ( [x,y] in R |^ A & [y,z] in R |^ A ) ; :: thesis: [x,z] in R |^ A

A7: now

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 )
[a,b] in R by A6, Def6;
then ( ( (p ^ <*a*>) ^ q in dom f implies (p ^ <*b*>) ^ q in dom f ) & ( (p ^ <*b*>) ^ q in dom f implies (p ^ <*a*>) ^ q in dom f ) & ( (p ^ <*a*>) ^ q in dom f & (p ^ <*b*>) ^ q in dom f implies [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*b*>) ^ q))] in R ) & ( (p ^ <*b*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f implies [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R ) ) by A1, A6, Def5, Def6;
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 EQREL_1:13; :: thesis: verum

end;

( [a,b] in R & [b,c] in R ) by A6, Def6;
then [a,c] in R by EQREL_1:13;
hence [x,z] in R |^ A by A7, Def6; :: thesis: verum

end;

then R |^ A is_transitive_in the carrier of A by RELAT_2:def 8;
hence R |^ A is transitive by A3, RELAT_2:def 16; :: thesis: verum