let A be partial non-empty UAStr ; :: thesis: for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds
for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive )
let R be Equivalence_Relation of the carrier of A; :: thesis: ( R c= DomRel A implies for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive ) )
assume A1: R c= DomRel A ; :: thesis: for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive )
defpred S₁[ Element of NAT ] means ( R |^ (A,$1) c= DomRel A & R |^ (A,$1) is total & R |^ (A,$1) is symmetric & R |^ (A,$1) is transitive );
A2: S₁[ 0 ] by A1, Th17;

A3: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
A5: (R |^ (A,i)) |^ A c= R |^ (A,i) by Th21;
(R |^ (A,i)) |^ A = R |^ (A,(i + 1)) by Th18;
hence S₁[i + 1] by A4, A5, Th20, XBOOLE_1:1; :: thesis: verum

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A2, A3);
hence for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive ) ; :: thesis: verum