let S be non empty non void ManySortedSign ; :: thesis:
let X be V5() ManySortedSet of S; :: thesis:
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X)); :: thesis:
let g be ManySortedFunction of (Free (S,X)),(Free (S,X)); :: thesis:
assume g is_homomorphism Free (S,X), Free (S,X) ; :: thesis:
let h be ManySortedFunction of (NFAlgebra R),(NFAlgebra R); :: thesis:
assume A1: for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ; :: thesis:
let s be SortSymbol of S; :: thesis:
let o be OperSymbol of S; :: thesis:
assume A2: s = the_result_sort_of o ; :: thesis:
let x be Element of Args (o,(NFAlgebra R)); :: thesis:
let y be Element of Args (o,(Free (S,X))); :: thesis:
assume A3: x = y ; :: thesis:
defpred S₁[ Nat] means ( $1 <= len (the_arity_of o) implies nf (((Den (o,(Free (S,X)))) . (((g # y) | $1) ^ ((h # x) /^ $1))),(R . s)) = nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) );
( dom (h # x) = dom (the_arity_of o) & dom (g # y) = dom (the_arity_of o) ) by MSUALG_3:6;
then A4: ( len (h # x) = len (the_arity_of o) & len (g # y) = len (the_arity_of o) ) by FINSEQ_3:29;
( (g # y) | 0 = {} & (h # x) /^ 0 = h # x ) by Th81;
then A5: ((g # y) | 0) ^ ((h # x) /^ 0) = h # x by FINSEQ_1:34;
A6: ( Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X))) & h # x in Args (o,(NFAlgebra R)) ) by Lm3;
then reconsider hx = h # x as Element of Args (o,(Free (S,X))) ;
( NForms R c= the Sorts of (Free (S,X)) & the Sorts of (NFAlgebra R) = NForms R ) by Def20, PBOOLE:def 18;
then ( Result (o,(Free (S,X))) = the Sorts of (Free (S,X)) . s & Result (o,(NFAlgebra R)) = the Sorts of (NFAlgebra R) . s & the Sorts of (NFAlgebra R) . s c= the Sorts of (Free (S,X)) . s & (Den (o,(NFAlgebra R))) . (h # x) in Result (o,(NFAlgebra R)) ) by A2, FUNCT_2:15;
then reconsider Dx = (Den (o,(Free (S,X)))) . hx, Dnx = (Den (o,(NFAlgebra R))) . (h # x) as Element of (Free (S,X)),s ;
nf ((nf (Dx,(R . s))),(R . s)) = nf (Dnx,(R . s)) by A2, Def20;
then A7: S₁[ 0 ] by A5, Th18;

A8: now :: thesis:

let i be Nat; :: thesis:
assume A9: S₁[i] ; :: thesis:
thus S₁[i + 1] :: thesis:

proof

assume A10: i + 1 <= len (the_arity_of o) ; :: thesis:
then A11: i < len (the_arity_of o) by NAT_1:13;
A12: ( len ((h # x) | i) = i & len ((g # y) | i) = i ) by A4, A11, FINSEQ_1:59;
A13: (g # y) | (i + 1) = ((g # y) | i) ^ <*((g # y) . (i + 1))*> by A4, A10, Th83;
A14: (h # x) /^ i = <*((h # x) . (i + 1))*> ^ ((h # x) /^ (i + 1)) by A4, A10, Th84;
A15: ( i + 1 in dom (the_arity_of o) & dom ( the Sorts of (NFAlgebra R) * (the_arity_of o)) = dom (the_arity_of o) ) by A10, NAT_1:11, FINSEQ_3:25, PRALG_2:3;
A16: ( x . (i + 1) in ( the Sorts of (NFAlgebra R) * (the_arity_of o)) . (i + 1) & (the_arity_of o) /. (i + 1) = (the_arity_of o) . (i + 1) ) by A15, PARTFUN1:def 6, MSUALG_3:6;
then reconsider xi1 = x . (i + 1) as Element of (NFAlgebra R),((the_arity_of o) /. (i + 1)) by A15, FUNCT_1:13;
dom x = dom (the_arity_of o) by MSUALG_3:6;
then (h # x) . (i + 1) = (h . ((the_arity_of o) /. (i + 1))) . xi1 by A15, MSUALG_3:def 6
.= nf (((g . ((the_arity_of o) /. (i + 1))) . xi1),(R . ((the_arity_of o) /. (i + 1)))) by A1 ;
then hx . (i + 1) is_a_normal_form_of (g . ((the_arity_of o) /. (i + 1))) . xi1,R . ((the_arity_of o) /. (i + 1)) by REWRITE1:54;
then A17: R . ((the_arity_of o) /. (i + 1)) reduces (g . ((the_arity_of o) /. (i + 1))) . xi1,hx . (i + 1) ;
A18: dom (h # x) = dom (the_arity_of o) by MSUALG_3:6;
then A19: len (h # x) = len (the_arity_of o) by FINSEQ_3:29;
defpred S₂[ set ] means nf (((Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*$1*>) ^ ((h # x) /^ (i + 1)))),(R . s)) = nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s));
A20: S₂[hx . (i + 1)] by A9, A10, NAT_1:13, A14, FINSEQ_1:32;
A21: for a, b being set st [a,b] in R . ((the_arity_of o) /. (i + 1)) & S₂[b] holds
S₂[a]

proof

let a, b be set ; :: thesis:
assume A22: [a,b] in R . ((the_arity_of o) /. (i + 1)) ; :: thesis:
then reconsider c = a, d = b as Element of the Sorts of (Free (S,X)) . ((the_arity_of o) /. (i + 1)) by ZFMISC_1:87;
reconsider j = i + 1 as Element of NAT by ORDINAL1:def 12;
set f = transl (o,j,((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),(Free (S,X)));

now :: thesis:

A23: len (((g # y) | i) ^ <*d*>) = i + (len <*d*>) by A12, FINSEQ_1:22
.= i + 1 by FINSEQ_1:40 ;
thus A24: dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3; :: thesis:
len ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) = (len (((g # y) | i) ^ <*d*>)) + (len ((h # x) /^ (i + 1))) by FINSEQ_1:22
.= (i + 1) + ((len (h # x)) - (i + 1)) by A10, A19, A23, RFINSEQ:def 1
.= len (the_arity_of o) by A18, FINSEQ_3:29 ;
hence dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) by A24, FINSEQ_3:29; :: thesis:
let a be object ; :: thesis:
assume A25: a in dom (the_arity_of o) ; :: thesis:
then reconsider b = a as Nat ;
A26: ( b <= len (the_arity_of o) & b >= 1 ) by A25, FINSEQ_3:25;

per cases by NAT_1:8;

suppose A27: b <= i ; :: thesis:

then A28: ( b in dom ((g # y) | i) & dom ((g # y) | i) c= dom (((g # y) | i) ^ <*d*>) & b in Seg i ) by A26, A12, FINSEQ_3:25, FINSEQ_1:26;
then ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a = (((g # y) | i) ^ <*d*>) . a by FINSEQ_1:def 7
.= ((g # y) | i) . a by A28, FINSEQ_1:def 7
.= (g # y) . a by A27, A26, FINSEQ_1:1, FUNCT_1:49 ;
hence ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a by A24, A25, MSUALG_3:6; :: thesis:

end;

suppose A29: b = i + 1 ; :: thesis:

then b in dom (((g # y) | i) ^ <*d*>) by A26, A23, FINSEQ_3:25;
then ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a = (((g # y) | i) ^ <*d*>) . a by FINSEQ_1:def 7
.= d by A12, A29, FINSEQ_1:42 ;
then ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a in the Sorts of (Free (S,X)) . ((the_arity_of o) /. (i + 1)) ;
hence ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a by A16, A25, A29, FUNCT_1:13; :: thesis:

end;

suppose A30: b > i + 1 ; :: thesis:

then consider k being Nat such that
A31: b = (i + 1) + k by NAT_1:10;
(i + 1) + k > (i + 1) + 0 by A30, A31;
then ( k > 0 & b - (i + 1) <= (len (the_arity_of o)) - (i + 1) ) by A26, XREAL_1:9, XREAL_1:6;
then ( k >= 0 + 1 & k <= len ((h # x) /^ (i + 1)) ) by A10, A19, RFINSEQ:def 1, A31, NAT_1:13;
then A32: k in dom ((h # x) /^ (i + 1)) by FINSEQ_3:25;
then ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a = ((h # x) /^ (i + 1)) . k by A23, A31, FINSEQ_1:def 7
.= (h # x) . a by A31, A19, A32, A10, RFINSEQ:def 1 ;
hence ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a by A24, A25, A6, MSUALG_3:6; :: thesis:

end;

then A33: (((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1)) in product ( the Sorts of (Free (S,X)) * (the_arity_of o)) by CARD_3:9;
then (((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1)) in Args (o,(Free (S,X))) by PRALG_2:3;
then A34: [((transl (o,j,((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),(Free (S,X)))) . c),((transl (o,j,((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),(Free (S,X)))) . d)] in R . s by A2, A15, A22, MSUALG_6:def 5, MSUALG_6:def 8;
reconsider ad = (((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1)) as Element of Args (o,(Free (S,X))) by A33, PRALG_2:3;
reconsider Dd = (Den (o,(Free (S,X)))) . ad as Element of (Free (S,X)),s by A2, FUNCT_2:15;
A35: (transl (o,j,((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),(Free (S,X)))) . c = (Den (o,(Free (S,X)))) . (((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) +* (j,c)) by MSUALG_6:def 4
.= (Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*c*>) ^ ((h # x) /^ (i + 1))) by A12, Th82 ;
(transl (o,j,((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),(Free (S,X)))) . d = (Den (o,(Free (S,X)))) . (((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) +* (j,d)) by MSUALG_6:def 4
.= (Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) by A12, Th82 ;
then A36: (Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*c*>) ^ ((h # x) /^ (i + 1))),(Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) are_convertible_wrt R . s by A34, A35, REWRITE1:29;
assume S₂[b] ; :: thesis:
hence S₂[a] by A36, REWRITE1:55; :: thesis:

end;

A37: S₂[(g . ((the_arity_of o) /. (i + 1))) . xi1] from MSAFREE4:sch 6(A20, A17, A21);
dom y = dom (the_arity_of o) by MSUALG_3:6;
hence nf (((Den (o,(Free (S,X)))) . (((g # y) | (i + 1)) ^ ((h # x) /^ (i + 1)))),(R . s)) = nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) by A13, A3, A15, A37, MSUALG_3:def 6; :: thesis:

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A7, A8);
then A38: nf (((Den (o,(Free (S,X)))) . (((g # y) | (len (the_arity_of o))) ^ ((h # x) /^ (len (the_arity_of o))))),(R . s)) = nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) ;
( (g # y) | (len (the_arity_of o)) = g # y & (h # x) /^ (len (the_arity_of o)) = {} ) by A4, FINSEQ_1:58, Th81;
hence nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s)) by A38, FINSEQ_1:34; :: thesis: