set X = the carrier of A;
DomRel A is_reflexive_in the carrier of A

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in the carrier of A or [x,x] in DomRel A )
for f being operation of A
for a, b being FinSequence holds
( (a ^ <*x*>) ^ b in dom f iff (a ^ <*x*>) ^ b in dom f ) ;
hence ( not x in the carrier of A or [x,x] in DomRel A ) by Def5; :: thesis: verum

end;

then A1: ( dom (DomRel A) = the carrier of A & field (DomRel A) = the carrier of A ) by ORDERS_1:98;
hence DomRel A is total by PARTFUN1:def 4; :: thesis: ( DomRel A is symmetric & DomRel A is transitive )
DomRel A is_symmetric_in the carrier of A

proof

let x, y be set ; :: according to RELAT_2:def 3 :: thesis: ( not x in the carrier of A or not y in the carrier of A or not [x,y] in DomRel A or [y,x] in DomRel A )
assume ( x in the carrier of A & y in the carrier of A ) ; :: thesis: ( not [x,y] in DomRel A or [y,x] in DomRel A )
then reconsider x' = x, y' = y as Element of the carrier of A ;
assume [x,y] in DomRel A ; :: thesis: [y,x] in DomRel A
then for f being operation of A
for a, b being FinSequence holds
( (a ^ <*x'*>) ^ b in dom f iff (a ^ <*y'*>) ^ b in dom f ) by Def5;
hence [y,x] in DomRel A by Def5; :: thesis: verum

end;

hence DomRel A is symmetric by A1, RELAT_2:def 11; :: thesis: DomRel A is transitive
DomRel A is_transitive_in the carrier of A

proof

let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in the carrier of A or not y in the carrier of A or not z in the carrier of A or not [x,y] in DomRel A or not [y,z] in DomRel A or [x,z] in DomRel A )
assume ( x in the carrier of A & y in the carrier of A & z in the carrier of A ) ; :: thesis: ( not [x,y] in DomRel A or not [y,z] in DomRel A or [x,z] in DomRel A )
then reconsider x' = x, y' = y, z' = z as Element of the carrier of A ;
assume A2: ( [x,y] in DomRel A & [y,z] in DomRel A ) ; :: thesis: [x,z] in DomRel A

now

let f be operation of A; :: thesis: for a, b being FinSequence holds
( (a ^ <*x'*>) ^ b in dom f iff (a ^ <*z'*>) ^ b in dom f )
let a, b be FinSequence; :: thesis: ( (a ^ <*x'*>) ^ b in dom f iff (a ^ <*z'*>) ^ b in dom f )
( (a ^ <*x'*>) ^ b in dom f iff (a ^ <*y'*>) ^ b in dom f ) by A2, Def5;
hence ( (a ^ <*x'*>) ^ b in dom f iff (a ^ <*z'*>) ^ b in dom f ) by A2, Def5; :: thesis: verum

end;

hence [x,z] in DomRel A by Def5; :: thesis: verum

end;

hence DomRel A is transitive by A1, RELAT_2:def 16; :: thesis: verum