let i be Nat; :: thesis: for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for t1, t2 being Element of (Free (S,X))
for p being Element of Args (o,(Free (S,X)))
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds
R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))
let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for t1, t2 being Element of (Free (S,X))
for p being Element of Args (o,(Free (S,X)))
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds
R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))
let o be OperSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t1, t2 being Element of (Free (S,X))
for p being Element of Args (o,(Free (S,X)))
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds
R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t1, t2 being Element of (Free (S,X))
for p being Element of Args (o,(Free (S,X)))
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds
R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))
let t1, t2 be Element of (Free (S,X)); :: thesis: for p being Element of Args (o,(Free (S,X)))
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds
R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))
let p be Element of Args (o,(Free (S,X))); :: thesis: for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds
R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))
let R be invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)); :: thesis: ( i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 implies R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2)) )
assume A1: ( i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 ) ; :: thesis: R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))
then consider r being RedSequence of R . ((the_arity_of o) /. i) such that
A2: ( r . 1 = t1 & r . (len r) = t2 ) ;
defpred S₁[ Nat] means ( $1 <= len r implies R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,(r . $1))) );
A3: S₁[1] by A2, REWRITE1:12;
A4: for i being Nat st 1 <= i & S₁[i] holds
S₁[i + 1]

proof

let k be Nat; :: thesis: ( 1 <= k & S₁[k] implies S₁[k + 1] )
assume A5: ( 1 <= k & S₁[k] & k + 1 <= len r ) ; :: thesis: R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,(r . (k + 1))))
( k < len r & 1 <= k + 1 ) by A5, NAT_1:13;
then ( k in dom r & k + 1 in dom r ) by A5, FINSEQ_3:25;
then A7: [(r . k),(r . (k + 1))] in R . ((the_arity_of o) /. i) by REWRITE1:def 2;
then reconsider rk = r . k, rk1 = r . (k + 1) as Element of the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) by ZFMISC_1:87;
reconsider p1 = p +* (i,rk), p2 = p +* (i,rk1) as Element of Args (o,(Free (S,X))) by MSUALG_6:7;
set h = transl (o,i,p,(Free (S,X)));
A10: ( dom p1 = dom (the_arity_of o) & dom (the_arity_of o) = dom p ) by MSUALG_6:2;
( (transl (o,i,p,(Free (S,X)))) . rk = (Den (o,(Free (S,X)))) . p1 & (transl (o,i,p,(Free (S,X)))) . rk1 = (Den (o,(Free (S,X)))) . p2 ) by MSUALG_6:def 4;
then [((Den (o,(Free (S,X)))) . p1),((Den (o,(Free (S,X)))) . p2)] in R . (the_result_sort_of o) by A7, A1, A10, MSUALG_6:def 5, MSUALG_6:def 8;
then R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . p1,(Den (o,(Free (S,X)))) . p2 by REWRITE1:15;
hence R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,(r . (k + 1)))) by A5, NAT_1:13, REWRITE1:16; :: thesis: verum

end;

A5: 0 + 1 <= len r by NAT_1:13;
for i being Nat st i >= 1 holds
S₁[i] from NAT_1:sch 8(A3, A4);
hence R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2)) by A2, A5; :: thesis: verum