set X = the carrier of A;
A1: DomRel A is_reflexive_in the carrier of A
proof
let x be object ; :: 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 Def4; :: thesis: verum
end;
then A2: dom (DomRel A) = the carrier of A by ORDERS_1:13;
A3: field (DomRel A) = the carrier of A by A1, ORDERS_1:13;
thus DomRel A is total by A2, PARTFUN1:def 2; :: thesis: ( DomRel A is symmetric & DomRel A is transitive )
DomRel A is_symmetric_in the carrier of A
proof
let x, y be object ; :: 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 that
A4: x in the carrier of A and
A5: y in the carrier of A ; :: thesis: ( not [x,y] in DomRel A or [y,x] in DomRel A )
reconsider x9 = x, y9 = y as Element of the carrier of A by A4, A5;
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 ^ <*x9*>) ^ b in dom f iff (a ^ <*y9*>) ^ b in dom f ) by Def4;
hence [y,x] in DomRel A by Def4; :: thesis: verum
end;
hence DomRel A is symmetric by A3; :: thesis: DomRel A is transitive
DomRel A is_transitive_in the carrier of A
proof
let x, y, z be object ; :: 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 that
A6: x in the carrier of A and
A7: y in the carrier of A and
A8: 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 )
reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of A by A6, A7, A8;
assume that
A9: [x,y] in DomRel A and
A10: [y,z] in DomRel A ; :: thesis: [x,z] in DomRel A
now :: thesis: for f being operation of A
for a, b being FinSequence holds
( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*z9*>) ^ b in dom f )
let f be operation of A; :: thesis: for a, b being FinSequence holds
( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*z9*>) ^ b in dom f )
let a, b be FinSequence; :: thesis: ( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*z9*>) ^ b in dom f )
( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*y9*>) ^ b in dom f ) by A9, Def4;
hence ( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*z9*>) ^ b in dom f ) by A10, Def4; :: thesis: verum
end;
hence [x,z] in DomRel A by Def4; :: thesis: verum
end;
hence DomRel A is transitive by A3; :: thesis: verum