let R1, R2 be Relation of F₁(),F₂(); :: thesis: ( ex F being ManySortedSet of st
( R1 = F . F₃() & F . 0 = F₄() & ( for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) ) & ex F being ManySortedSet of st
( R2 = F . F₃() & F . 0 = F₄() & ( for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) ) implies R1 = R2 )
given F1 being ManySortedSet of such that A1: ( R1 = F1 . F₃() & F1 . 0 = F₄() & ( for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F1 . i holds
F1 . (i + 1) = F₅(R,i) ) ) ; :: thesis: ( for F being ManySortedSet of holds
( not R2 = F . F₃() or not F . 0 = F₄() or ex i being Element of NAT ex R being Relation of F₁(),F₂() st
( R = F . i & not F . (i + 1) = F₅(R,i) ) ) or R1 = R2 )
given F2 being ManySortedSet of such that A2: ( R2 = F2 . F₃() & F2 . 0 = F₄() & ( for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F2 . i holds
F2 . (i + 1) = F₅(R,i) ) ) ; :: thesis: R1 = R2
defpred S₁[ Element of NAT ] means ( F1 . $1 = F2 . $1 & F1 . $1 is Relation of F₁(),F₂() );
A3: S₁[ 0 ] by A1, A2;

A4: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
then reconsider R = F1 . i as Relation of F₁(),F₂() ;
( F1 . (i + 1) = F₅(R,i) & F2 . (i + 1) = F₅(R,i) ) by A1, A2, A5;
hence S₁[i + 1] ; :: thesis: verum

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A3, A4);
hence R1 = R2 by A1, A2; :: thesis: verum