defpred S1[ DecoratedTree, Function] means ( dom $2 = Subtrees $1 & ( for s being SortSymbol of F1()
for x being Element of F2() . s st root-tree [x,s] in Subtrees $1 holds
$2 . (root-tree [x,s]) = F3(x,s) ) & ( for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st (Sym (o,F2())) -tree p in Subtrees $1 holds
$2 . ((Sym (o,F2())) -tree p) = F4(o,($2 * p)) ) );
defpred S2[ DecoratedTree] means ex f being Function st S1[$1,f];
A1: for t1, t2 being Term of F1(),F2()
for f1, f2 being Function st S1[t1,f1] & S1[t2,f2] holds
f1 tolerates f2
proof
let t1, t2 be Term of F1(),F2(); :: thesis: for f1, f2 being Function st S1[t1,f1] & S1[t2,f2] holds
f1 tolerates f2
let f1, f2 be Function; :: thesis: ( S1[t1,f1] & S1[t2,f2] implies f1 tolerates f2 )
assume A2: ( S1[t1,f1] & S1[t2,f2] ) ; :: thesis: f1 tolerates f2
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 f1) /\ (proj1 f2) or f1 . x = f2 . x )
assume x in (dom f1) /\ (dom f2) ; :: thesis: f1 . x = f2 . x
then A3: ( x in Subtrees t1 & x in Subtrees t2 ) by A2, XBOOLE_0:def 4;
then A4: ex r being Element of dom t1 st x = t1 | r ;
defpred S3[ DecoratedTree] means ( $1 in Subtrees t1 & $1 in Subtrees t2 implies f1 . $1 = f2 . $1 );
A5: for s being SortSymbol of F1()
for v being Element of F2() . s holds S3[ root-tree [v,s]]
proof
let s be SortSymbol of F1(); :: thesis: for v being Element of F2() . s holds S3[ root-tree [v,s]]
let x be Element of F2() . s; :: thesis: S3[ root-tree [x,s]]
assume A6: ( root-tree [x,s] in Subtrees t1 & root-tree [x,s] in Subtrees t2 ) ; :: thesis: f1 . (root-tree [x,s]) = f2 . (root-tree [x,s])
then f1 . (root-tree [x,s]) = F3(x,s) by A2;
hence f1 . (root-tree [x,s]) = f2 . (root-tree [x,s]) by A6, A2; :: thesis: verum
end;
A7: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st ( for t being Term of F1(),F2() st t in rng p holds
S3[t] ) holds
S3[[o, the carrier of F1()] -tree p]
proof
let o be OperSymbol of F1(); :: thesis: for p being ArgumentSeq of Sym (o,F2()) st ( for t being Term of F1(),F2() st t in rng p holds
S3[t] ) holds
S3[[o, the carrier of F1()] -tree p]
let p be ArgumentSeq of Sym (o,F2()); :: thesis: ( ( for t being Term of F1(),F2() st t in rng p holds
S3[t] ) implies S3[[o, the carrier of F1()] -tree p] )
assume A8: for t being Term of F1(),F2() st t in rng p holds
S3[t] ; :: thesis: S3[[o, the carrier of F1()] -tree p]
set t = [o, the carrier of F1()] -tree p;
assume A9: ( [o, the carrier of F1()] -tree p in Subtrees t1 & [o, the carrier of F1()] -tree p in Subtrees t2 ) ; :: thesis: f1 . ([o, the carrier of F1()] -tree p) = f2 . ([o, the carrier of F1()] -tree p)
rng p c= Subtrees t1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in Subtrees t1 )
assume A10: x in rng p ; :: thesis: x in Subtrees t1
then consider y being object such that
A11: ( y in dom p & x = p . y ) by FUNCT_1:def 3;
reconsider y = y as Nat by A11;
consider n being Nat such that
A12: y = 1 + n by A11, FINSEQ_3:25, NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
rng p c= F1() -Terms F2() by FINSEQ_1:def 4;
then reconsider tn = p . y as Term of F1(),F2() by A11, A10;
reconsider q = {} as Element of dom tn by TREES_1:22;
consider r being Element of dom t1 such that
A13: [o, the carrier of F1()] -tree p = t1 | r by A9;
n + 1 <= len p by A11, A12, FINSEQ_3:25;
then ( n < len p & <*n*> ^ q = <*n*> ) by NAT_1:13, FINSEQ_1:34;
then ( ([o, the carrier of F1()] -tree p) | <*n*> = x & <*n*> in dom ([o, the carrier of F1()] -tree p) ) by A11, A12, TREES_4:def 4, TREES_4:11;
then ( x in Subtrees ([o, the carrier of F1()] -tree p) & Subtrees ([o, the carrier of F1()] -tree p) c= Subtrees t1 ) by A13, TREES_9:13;
hence x in Subtrees t1 ; :: thesis: verum
end;
then A14: dom (f1 * p) = dom p by A2, RELAT_1:27;
rng p c= Subtrees t2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in Subtrees t2 )
assume A15: x in rng p ; :: thesis: x in Subtrees t2
then consider y being object such that
A16: ( y in dom p & x = p . y ) by FUNCT_1:def 3;
reconsider y = y as Nat by A16;
consider n being Nat such that
A17: y = 1 + n by A16, FINSEQ_3:25, NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
rng p c= F1() -Terms F2() by FINSEQ_1:def 4;
then reconsider tn = p . y as Term of F1(),F2() by A16, A15;
reconsider q = {} as Element of dom tn by TREES_1:22;
consider r being Element of dom t2 such that
A18: [o, the carrier of F1()] -tree p = t2 | r by A9;
n + 1 <= len p by A16, A17, FINSEQ_3:25;
then ( n < len p & <*n*> ^ q = <*n*> ) by NAT_1:13, FINSEQ_1:34;
then ( ([o, the carrier of F1()] -tree p) | <*n*> = x & <*n*> in dom ([o, the carrier of F1()] -tree p) ) by A16, A17, TREES_4:def 4, TREES_4:11;
then ( x in Subtrees ([o, the carrier of F1()] -tree p) & Subtrees ([o, the carrier of F1()] -tree p) c= Subtrees t2 ) by A18, TREES_9:13;
hence x in Subtrees t2 ; :: thesis: verum
end;
then A19: dom (f2 * p) = dom p by A2, RELAT_1:27;
now :: thesis: for x being object st x in dom p holds
(f1 * p) . x = (f2 * p) . x
let x be object ; :: thesis: ( x in dom p implies (f1 * p) . x = (f2 * p) . x )
assume A20: x in dom p ; :: thesis: (f1 * p) . x = (f2 * p) . x
then A21: p . x in rng p by FUNCT_1:def 3;
rng p c= F1() -Terms F2() by FINSEQ_1:def 4;
then reconsider w = p . x as Term of F1(),F2() by A21;
A22: S3[w] by A8, A21;
reconsider y = x as Nat by A20;
consider n being Nat such that
A23: y = 1 + n by A20, FINSEQ_3:25, NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider q = {} as Element of dom w by TREES_1:22;
consider r1 being Element of dom t1 such that
A24: [o, the carrier of F1()] -tree p = t1 | r1 by A9;
consider r2 being Element of dom t2 such that
A25: [o, the carrier of F1()] -tree p = t2 | r2 by A9;
n + 1 <= len p by A20, A23, FINSEQ_3:25;
then ( n < len p & <*n*> ^ q = <*n*> ) by NAT_1:13, FINSEQ_1:34;
then ( ([o, the carrier of F1()] -tree p) | <*n*> = w & <*n*> in dom ([o, the carrier of F1()] -tree p) ) by A23, TREES_4:def 4, TREES_4:11;
then ( w in Subtrees ([o, the carrier of F1()] -tree p) & Subtrees ([o, the carrier of F1()] -tree p) c= Subtrees t2 & Subtrees ([o, the carrier of F1()] -tree p) c= Subtrees t1 ) by A24, A25, TREES_9:13;
hence (f1 * p) . x = f2 . w by A20, A22, FUNCT_1:13
.= (f2 * p) . x by A20, FUNCT_1:13 ;
:: thesis: verum
end;
then f1 * p = f2 * p by A14, A19;
hence f1 . ([o, the carrier of F1()] -tree p) = F4(o,(f2 * p)) by A2, A9
.= f2 . ([o, the carrier of F1()] -tree p) by A2, A9 ;
:: thesis: verum
end;
for t being Term of F1(),F2() holds S3[t] from MSATERM:sch 1(A5, A7);
 hence f1 . x = f2 . x by A3, A4; :: thesis: verum
end;
A26: for s being SortSymbol of F1()
for v being Element of F2() . s holds S2[ root-tree [v,s]]
proof
let s be SortSymbol of F1(); :: thesis: for v being Element of F2() . s holds S2[ root-tree [v,s]]
let x be Element of F2() . s; :: thesis: S2[ root-tree [x,s]]
A27: Subtrees (root-tree [x,s]) = {(root-tree [x,s])} by Th2;
take f = {(root-tree [x,s])} --> F3(x,s); :: thesis: S1[ root-tree [x,s],f]
thus dom f = Subtrees (root-tree [x,s]) by A27; :: thesis: ( ( for s being SortSymbol of F1()
for x being Element of F2() . s st root-tree [x,s] in Subtrees (root-tree [x,s]) holds
f . (root-tree [x,s]) = F3(x,s) ) & ( for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st (Sym (o,F2())) -tree p in Subtrees (root-tree [x,s]) holds
f . ((Sym (o,F2())) -tree p) = F4(o,(f * p)) ) )
hereby :: thesis: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st (Sym (o,F2())) -tree p in Subtrees (root-tree [x,s]) holds
f . ((Sym (o,F2())) -tree p) = F4(o,(f * p))
let s1 be SortSymbol of F1(); :: thesis: for x1 being Element of F2() . s1 st root-tree [x1,s1] in Subtrees (root-tree [x,s]) holds
f . (root-tree [x1,s1]) = F3(x1,s1)
let x1 be Element of F2() . s1; :: thesis: ( root-tree [x1,s1] in Subtrees (root-tree [x,s]) implies f . (root-tree [x1,s1]) = F3(x1,s1) )
assume A28: root-tree [x1,s1] in Subtrees (root-tree [x,s]) ; :: thesis: f . (root-tree [x1,s1]) = F3(x1,s1)
then root-tree [x1,s1] = root-tree [x,s] by A27, TARSKI:def 1;
then [x1,s1] = [x,s] by TREES_4:4;
then ( x1 = x & s1 = s ) by XTUPLE_0:1;
hence f . (root-tree [x1,s1]) = F3(x1,s1) by A27, A28, FUNCOP_1:7; :: thesis: verum
end;
let o be OperSymbol of F1(); :: thesis: for p being ArgumentSeq of Sym (o,F2()) st (Sym (o,F2())) -tree p in Subtrees (root-tree [x,s]) holds
f . ((Sym (o,F2())) -tree p) = F4(o,(f * p))
let p be ArgumentSeq of Sym (o,F2()); :: thesis: ( (Sym (o,F2())) -tree p in Subtrees (root-tree [x,s]) implies f . ((Sym (o,F2())) -tree p) = F4(o,(f * p)) )
assume (Sym (o,F2())) -tree p in Subtrees (root-tree [x,s]) ; :: thesis: f . ((Sym (o,F2())) -tree p) = F4(o,(f * p))
then (Sym (o,F2())) -tree p = root-tree [x,s] by A27, TARSKI:def 1;
then Sym (o,F2()) = [x,s] by TREES_4:17;
then ( s = the carrier of F1() & s in the carrier of F1() ) by XTUPLE_0:1;
hence f . ((Sym (o,F2())) -tree p) = F4(o,(f * p)) ; :: thesis: verum
end;
A29: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st ( for t being Term of F1(),F2() st t in rng p holds
S2[t] ) holds
S2[[o, the carrier of F1()] -tree p]
proof
let o be OperSymbol of F1(); :: thesis: for p being ArgumentSeq of Sym (o,F2()) st ( for t being Term of F1(),F2() st t in rng p holds
S2[t] ) holds
S2[[o, the carrier of F1()] -tree p]
let p be ArgumentSeq of Sym (o,F2()); :: thesis: ( ( for t being Term of F1(),F2() st t in rng p holds
S2[t] ) implies S2[[o, the carrier of F1()] -tree p] )
assume A30: for t being Term of F1(),F2() st t in rng p holds
S2[t] ; :: thesis: S2[[o, the carrier of F1()] -tree p]
defpred S3[ object , object ] means ex f being Function ex t being Term of F1(),F2() st
( t = p . $1 & $2 = f & S1[t,f] );
A31: for x being object st x in dom p holds
ex y being object st S3[x,y]
proof
let x be object ; :: thesis: ( x in dom p implies ex y being object st S3[x,y] )
assume x in dom p ; :: thesis: ex y being object st S3[x,y]
then A32: ( p . x in rng p & rng p c= F1() -Terms F2() ) by FUNCT_1:def 3, FINSEQ_1:def 4;
then reconsider t = p . x as Term of F1(),F2() ;
consider f being Function such that
A33: S1[t,f] by A30, A32;
take f ; :: thesis: S3[x,f]
take f ; :: thesis: ex t being Term of F1(),F2() st
( t = p . x & f = f & S1[t,f] )
take t ; :: thesis: ( t = p . x & f = f & S1[t,f] )
thus ( t = p . x & f = f & S1[t,f] ) by A33; :: thesis: verum
end;
consider g being Function such that
A34: ( dom g = dom p & ( for x being object st x in dom p holds
S3[x,g . x] ) ) from CLASSES1:sch 1(A31);
A35: now :: thesis: ( rng g is functional & ( for x, y being Function st x in rng g & y in rng g holds
x tolerates y ) )
thus rng g is functional :: thesis: for x, y being Function st x in rng g & y in rng g holds
x tolerates y
proof
let y be object ; :: according to FUNCT_1:def 13 :: thesis: ( not y in rng g or y is set )
assume y in rng g ; :: thesis: y is set
then consider x being object such that
A36: ( x in dom g & y = g . x ) by FUNCT_1:def 3;
S3[x,y] by A34, A36;
hence y is set ; :: thesis: verum
end;
let x, y be Function; :: thesis: ( x in rng g & y in rng g implies x tolerates y )
assume A37: ( x in rng g & y in rng g ) ; :: thesis: x tolerates y
then consider x0 being object such that
A38: ( x0 in dom g & x = g . x0 ) by FUNCT_1:def 3;
consider y0 being object such that
A39: ( y0 in dom g & y = g . y0 ) by A37, FUNCT_1:def 3;
( S3[x0,x] & S3[y0,y] ) by A34, A38, A39;
hence x tolerates y by A1; :: thesis: verum
end;
then reconsider f1 = union (rng g) as Function by PARTFUN1:78;
set t = [o, the carrier of F1()] -tree p;
set f = f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)));
take f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) ; :: thesis: S1[[o, the carrier of F1()] -tree p,f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))]
defpred S4[ object , object ] means ex I being set st
( I = $1 & $2 = proj1 I );
A40: for x, y, z being object st S4[x,y] & S4[x,z] holds
y = z ;
consider Y being set such that
A41: for x being object holds
( x in Y iff ex y being object st
( y in rng g & S4[y,x] ) ) from TARSKI:sch 1(A40);
 A42: dom f1 = union Y
proof
thus dom f1 c= union Y :: according to XBOOLE_0:def 10 :: thesis: union Y c= dom f1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f1 or x in union Y )
assume x in dom f1 ; :: thesis: x in union Y
then [x,(f1 . x)] in f1 by FUNCT_1:1;
then consider Z being set such that
A43: ( [x,(f1 . x)] in Z & Z in rng g ) by TARSKI:def 4;
( x in proj1 Z & proj1 Z in Y ) by A43, A41, XTUPLE_0:def 12;
hence x in union Y by TARSKI:def 4; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union Y or z in dom f1 )
assume z in union Y ; :: thesis: z in dom f1
then consider Z being set such that
A44: ( z in Z & Z in Y ) by TARSKI:def 4;
consider y being object such that
A45: ( y in rng g & ex I being set st
( I = y & Z = proj1 I ) ) by A44, A41;
reconsider y = y as Function by A45, A35;
[z,(y . z)] in y by A44, A45, FUNCT_1:1;
then [z,(y . z)] in f1 by A45, TARSKI:def 4;
hence z in dom f1 by FUNCT_1:1; :: thesis: verum
end;
A46: dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) = (dom f1) \/ (dom ({((Sym (o,F2())) -tree p)} --> F4(o,(f1 * p)))) by FUNCT_4:def 1
.= (dom f1) \/ {((Sym (o,F2())) -tree p)} ;
dom f1 misses dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))
proof
set x = the Element of (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))));
assume (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then A47: ( the Element of (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) in dom f1 & the Element of (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) in dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) ) by XBOOLE_0:def 4;
then [ the Element of (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))),(f1 . the Element of (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))))] in f1 by FUNCT_1:1;
then consider Y being set such that
A48: ( [ the Element of (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))),(f1 . the Element of (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))))] in Y & Y in rng g ) by TARSKI:def 4;
consider y being object such that
A49: ( y in dom g & Y = g . y ) by A48, FUNCT_1:def 3;
A50: S3[y,Y] by A34, A49;
then reconsider t1 = p . y as Term of F1(),F2() ;
( the Element of (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) in Subtrees t1 & t1 in rng p ) by A34, A49, A48, A50, XTUPLE_0:def 12, FUNCT_1:def 3;
then the Element of (dom f1) /\ (dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) <> [o, the carrier of F1()] -tree p by Th7;
hence contradiction by A47, TARSKI:def 1; :: thesis: verum
end;
then A51: f1 c= f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) by FUNCT_4:28, PARTFUN1:56;
per cases ( p = {} or p <> {} ) ;
suppose A52: p = {} ; :: thesis: S1[[o, the carrier of F1()] -tree p,f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))]
then A53: Subtrees ((Sym (o,F2())) -tree p) = {((Sym (o,F2())) -tree p)} by Th4;
dom p = {} by A52;
then rng g = {} by A34, RELAT_1:42;
hence dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) = {} \/ (Subtrees ([o, the carrier of F1()] -tree p)) by A53, A46, ZFMISC_1:2
.= Subtrees ([o, the carrier of F1()] -tree p) ;
:: thesis: ( ( for s being SortSymbol of F1()
for x being Element of F2() . s st root-tree [x,s] in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s) ) & ( for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st (Sym (o,F2())) -tree p in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o,F2())) -tree p) = F4(o,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p)) ) )
hereby :: thesis: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st (Sym (o,F2())) -tree p in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o,F2())) -tree p) = F4(o,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p))
let s be SortSymbol of F1(); :: thesis: for x being Element of F2() . s st root-tree [x,s] in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s)
let x be Element of F2() . s; :: thesis: ( root-tree [x,s] in Subtrees ([o, the carrier of F1()] -tree p) implies (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s) )
assume root-tree [x,s] in Subtrees ([o, the carrier of F1()] -tree p) ; :: thesis: (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s)
then root-tree [x,s] = [o, the carrier of F1()] -tree p by A53, TARSKI:def 1;
then [x,s] = Sym (o,F2()) by TREES_4:17;
then ( s = the carrier of F1() & s in the carrier of F1() ) by XTUPLE_0:1;
hence (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s) ; :: thesis: verum
end;
let o0 be OperSymbol of F1(); :: thesis: for p being ArgumentSeq of Sym (o0,F2()) st (Sym (o0,F2())) -tree p in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o0,F2())) -tree p) = F4(o0,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p))
let p0 be ArgumentSeq of Sym (o0,F2()); :: thesis: ( (Sym (o0,F2())) -tree p0 in Subtrees ([o, the carrier of F1()] -tree p) implies (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o0,F2())) -tree p0) = F4(o0,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p0)) )
assume (Sym (o0,F2())) -tree p0 in Subtrees ([o, the carrier of F1()] -tree p) ; :: thesis: (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o0,F2())) -tree p0) = F4(o0,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p0))
then A54: (Sym (o0,F2())) -tree p0 = [o, the carrier of F1()] -tree p by A53, TARSKI:def 1;
(rng p) /\ (dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))))) c= dom f1
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (rng p) /\ (dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))))) or z in dom f1 )
assume z in (rng p) /\ (dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))))) ; :: thesis: z in dom f1
then A55: ( z in rng p & rng p c= F1() -Terms F2() ) by XBOOLE_0:def 4, FINSEQ_1:def 4;
then reconsider z = z as Term of F1(),F2() ;
consider y being object such that
A56: ( y in dom p & z = p . y ) by A55, FUNCT_1:def 3;
S3[y,g . y] by A34, A56;
then A57: ( z in proj1 (g . y) & g . y in rng g ) by A34, A56, TREES_9:11, FUNCT_1:def 3;
then proj1 (g . y) in Y by A41;
hence z in dom f1 by A42, A57, TARSKI:def 4; :: thesis: verum
end;
then A58: f1 * p = (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p by A51, ALGSPEC1:2;
( Sym (o0,F2()) = Sym (o,F2()) & p = p0 ) by A54, TREES_4:15;
then A59: ( p0 = p & o0 = o ) by XTUPLE_0:1;
A60: [o, the carrier of F1()] -tree p in {([o, the carrier of F1()] -tree p)} by TARSKI:def 1;
[o, the carrier of F1()] -tree p in dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) by TARSKI:def 1;
hence (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o0,F2())) -tree p0) = ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) . ([o, the carrier of F1()] -tree p) by A54, FUNCT_4:13
.= F4(o0,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p0)) by A58, A59, A60, FUNCOP_1:7 ;
:: thesis: verum
end;
suppose p <> {} ; :: thesis: S1[[o, the carrier of F1()] -tree p,f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))]
then reconsider p = p as non empty DTree-yielding FinSequence ;
A61: union Y = Subtrees (rng p)
proof
thus union Y c= Subtrees (rng p) :: according to XBOOLE_0:def 10 :: thesis: Subtrees (rng p) c= union Y
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union Y or z in Subtrees (rng p) )
assume z in union Y ; :: thesis: z in Subtrees (rng p)
then consider W being set such that
A62: ( z in W & W in Y ) by TARSKI:def 4;
consider y being object such that
A63: ( y in rng g & S4[y,W] ) by A62, A41;
consider a being object such that
A64: ( a in dom g & y = g . a ) by A63, FUNCT_1:def 3;
reconsider a = a as Nat by A34, A64;
consider f being Function, t being Term of F1(),F2() such that
A65: ( t = p . a & y = f & S1[t,f] ) by A34, A64;
( W = Subtrees t & t in rng p ) by A34, A63, A64, A65, FUNCT_1:def 3;
then W c= Subtrees (rng p) by Th8;
hence z in Subtrees (rng p) by A62; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Subtrees (rng p) or z in union Y )
assume z in Subtrees (rng p) ; :: thesis: z in union Y
then consider t being Element of rng p, q being Element of dom t such that
A66: z = t | q ;
A67: z in Subtrees t by A66;
consider a being object such that
A68: ( a in dom p & t = p . a ) by FUNCT_1:def 3;
reconsider a = a as Nat by A68;
consider f3 being Function, t1 being Term of F1(),F2() such that
A69: ( t1 = p . a & g . a = f3 & S1[t1,f3] ) by A68, A34;
f3 in rng g by A34, A68, A69, FUNCT_1:def 3;
then Subtrees t in Y by A68, A69, A41;
hence z in union Y by A67, TARSKI:def 4; :: thesis: verum
end;
dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) = {([o, the carrier of F1()] -tree p)} ;
then dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) = (union Y) \/ {([o, the carrier of F1()] -tree p)} by A42, FUNCT_4:def 1;
hence dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) = Subtrees ([o, the carrier of F1()] -tree p) by A61, Th3; :: thesis: ( ( for s being SortSymbol of F1()
for x being Element of F2() . s st root-tree [x,s] in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s) ) & ( for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st (Sym (o,F2())) -tree p in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o,F2())) -tree p) = F4(o,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p)) ) )
hereby :: thesis: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st (Sym (o,F2())) -tree p in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o,F2())) -tree p) = F4(o,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p))
let s be SortSymbol of F1(); :: thesis: for x being Element of F2() . s st root-tree [x,s] in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s)
let x be Element of F2() . s; :: thesis: ( root-tree [x,s] in Subtrees ([o, the carrier of F1()] -tree p) implies (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s) )
assume A70: root-tree [x,s] in Subtrees ([o, the carrier of F1()] -tree p) ; :: thesis: (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s)
s in the carrier of F1() ;
then s <> the carrier of F1() ;
then [x,s] <> Sym (o,F2()) by XTUPLE_0:1;
then A71: root-tree [x,s] <> [o, the carrier of F1()] -tree p by TREES_4:17;
then ( root-tree [x,s] nin {([o, the carrier of F1()] -tree p)} & Subtrees ([o, the carrier of F1()] -tree p) = {([o, the carrier of F1()] -tree p)} \/ (Subtrees (rng p)) ) by Th3, TARSKI:def 1;
then root-tree [x,s] in Subtrees (rng p) by A70, XBOOLE_0:def 3;
then consider h being Element of rng p, r being Element of dom h such that
A72: root-tree [x,s] = h | r ;
( h in rng p & rng p c= F1() -Terms F2() ) by FINSEQ_1:def 4;
then reconsider h = h as Term of F1(),F2() ;
consider f2 being Function such that
A73: S1[h,f2] by A30;
consider a being object such that
A74: ( a in dom p & h = p . a ) by FUNCT_1:def 3;
reconsider a = a as Nat by A74;
consider f3 being Function, t1 being Term of F1(),F2() such that
A75: ( t1 = p . a & g . a = f3 & S1[t1,f3] ) by A74, A34;
A76: f3 = f2 by A73, A74, A75, A1, PARTFUN1:55;
A77: root-tree [x,s] in Subtrees h by A72;
then f2 . (root-tree [x,s]) = F3(x,s) by A73;
then ( [(root-tree [x,s]),F3(x,s)] in f2 & f2 in rng g ) by A77, A74, A75, A76, A34, FUNCT_1:1, FUNCT_1:def 3;
then [(root-tree [x,s]),F3(x,s)] in f1 by TARSKI:def 4;
then ( f1 . (root-tree [x,s]) = F3(x,s) & root-tree [x,s] nin dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) ) by A71, TARSKI:def 1, FUNCT_1:1;
hence (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . (root-tree [x,s]) = F3(x,s) by FUNCT_4:11; :: thesis: verum
end;
let o1 be OperSymbol of F1(); :: thesis: for p being ArgumentSeq of Sym (o1,F2()) st (Sym (o1,F2())) -tree p in Subtrees ([o, the carrier of F1()] -tree p) holds
(f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o1,F2())) -tree p) = F4(o1,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p))
let p1 be ArgumentSeq of Sym (o1,F2()); :: thesis: ( (Sym (o1,F2())) -tree p1 in Subtrees ([o, the carrier of F1()] -tree p) implies (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o1,F2())) -tree p1) = F4(o1,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p1)) )
set t1 = (Sym (o1,F2())) -tree p1;
assume (Sym (o1,F2())) -tree p1 in Subtrees ([o, the carrier of F1()] -tree p) ; :: thesis: (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o1,F2())) -tree p1) = F4(o1,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p1))
then A78: (Sym (o1,F2())) -tree p1 in {([o, the carrier of F1()] -tree p)} \/ (Subtrees (rng p)) by Th3;
( rng p c= Subtrees (rng p) & (rng p) /\ (dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))))) c= rng p ) by Th9, XBOOLE_1:17;
then (rng p) /\ (dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))))) c= dom f1 by A42, A61;
then A79: f1 * p = (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p by A51, ALGSPEC1:2;
per cases ( (Sym (o1,F2())) -tree p1 in {([o, the carrier of F1()] -tree p)} or (Sym (o1,F2())) -tree p1 in union Y ) by A78, A61, XBOOLE_0:def 3;
suppose A80: (Sym (o1,F2())) -tree p1 in {([o, the carrier of F1()] -tree p)} ; :: thesis: (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o1,F2())) -tree p1) = F4(o1,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p1))
then (Sym (o1,F2())) -tree p1 = [o, the carrier of F1()] -tree p by TARSKI:def 1;
then A81: ( Sym (o,F2()) = Sym (o1,F2()) & p = p1 ) by TREES_4:15;
dom ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) = {([o, the carrier of F1()] -tree p)} ;
then (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o1,F2())) -tree p1) = ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) . ((Sym (o1,F2())) -tree p1) by A80, FUNCT_4:13
.= F4(o,(f1 * p)) by A80, FUNCOP_1:7 ;
hence (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o1,F2())) -tree p1) = F4(o1,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p1)) by A81, A79, XTUPLE_0:1; :: thesis: verum
end;
suppose (Sym (o1,F2())) -tree p1 in union Y ; :: thesis: (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o1,F2())) -tree p1) = F4(o1,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p1))
then consider W being set such that
A82: ( (Sym (o1,F2())) -tree p1 in W & W in Y ) by TARSKI:def 4;
consider y being object such that
A83: ( y in rng g & S4[y,W] ) by A41, A82;
consider z being object such that
A84: ( z in dom g & y = g . z ) by A83, FUNCT_1:def 3;
reconsider z = z as Nat by A34, A84;
consider f2 being Function, t2 being Term of F1(),F2() such that
A85: ( t2 = p . z & y = f2 & S1[t2,f2] ) by A34, A84;
A86: f2 . ((Sym (o1,F2())) -tree p1) = F4(o1,(f2 * p1)) by A85, A82, A83;
A87: ( rng p1 c= Subtrees ((Sym (o1,F2())) -tree p1) & (rng p1) /\ (dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))))) c= rng p1 ) by XBOOLE_1:17, Th11;
Subtrees ((Sym (o1,F2())) -tree p1) c= Subtrees t2 by A82, A83, A85, Th12;
then A88: rng p1 c= dom f2 by A87, A85;
f2 c= f1 by A83, A85, ZFMISC_1:74;
then A89: ( (rng p1) /\ (dom (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))))) c= dom f2 & f2 c= f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p))) ) by A51, A87, A88;
thus (f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) . ((Sym (o1,F2())) -tree p1) = f2 . ((Sym (o1,F2())) -tree p1) by A82, A83, A89, A85, FOMODEL0:51
.= F4(o1,((f1 +* ({([o, the carrier of F1()] -tree p)} --> F4(o,(f1 * p)))) * p1)) by A86, A89, ALGSPEC1:2 ; :: thesis: verum
end;
end;
end;
end;
end;
A90: for t being Term of F1(),F2() holds S2[t] from MSATERM:sch 1(A26, A29);
 defpred S3[ object , object ] means ex t being Term of F1(),F2() ex f being Function st
( t = $1 & f = $2 & S1[t,f] );
A91: for x being object st x in F1() -Terms F2() holds
ex y being object st S3[x,y]
proof
let x be object ; :: thesis: ( x in F1() -Terms F2() implies ex y being object st S3[x,y] )
assume x in F1() -Terms F2() ; :: thesis: ex y being object st S3[x,y]
then reconsider t = x as Term of F1(),F2() ;
S2[t] by A90;
hence ex y being object st S3[x,y] ; :: thesis: verum
end;
consider F being Function such that
A92: ( dom F = F1() -Terms F2() & ( for x being object st x in F1() -Terms F2() holds
S3[x,F . x] ) ) from CLASSES1:sch 1(A91);
 ( rng F is functional & rng F is compatible )
proof
thus rng F is functional :: thesis: rng F is compatible
proof
let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in rng F or x is set )
assume x in rng F ; :: thesis: x is set
then consider x0 being object such that
A93: ( x0 in dom F & x = F . x0 ) by FUNCT_1:def 3;
S3[x0,x] by A92, A93;
hence x is set ; :: thesis: verum
end;
let h1, h2 be Function; :: according to COMPUT_1:def 1 :: thesis: ( not h1 in rng F or not h2 in rng F or h1 tolerates h2 )
assume A94: ( h1 in rng F & h2 in rng F ) ; :: thesis: h1 tolerates h2
then consider x0 being object such that
A95: ( x0 in dom F & h1 = F . x0 ) by FUNCT_1:def 3;
consider y0 being object such that
A96: ( y0 in dom F & h2 = F . y0 ) by A94, FUNCT_1:def 3;
( S3[x0,h1] & S3[y0,h2] ) by A92, A95, A96;
hence h1 tolerates h2 by A1; :: thesis: verum
end;
then reconsider rF = rng F as non empty functional compatible set by A92, RELAT_1:42;
reconsider f = union rF as Function ;
dom f = F1() -Terms F2()
proof
A97: dom f = union { (dom h) where h is Element of rF : verum } by COMPUT_1:12;
thus dom f c= F1() -Terms F2() :: according to XBOOLE_0:def 10 :: thesis: F1() -Terms F2() c= dom f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in F1() -Terms F2() )
assume x in dom f ; :: thesis: x in F1() -Terms F2()
then consider W being set such that
A98: ( x in W & W in { (dom h) where h is Element of rF : verum } ) by A97, TARSKI:def 4;
consider h being Element of rF such that
A99: W = dom h by A98;
consider x0 being object such that
A100: ( x0 in dom F & h = F . x0 ) by FUNCT_1:def 3;
reconsider x0 = x0 as Term of F1(),F2() by A92, A100;
S3[x0,h] by A92, A100;
then x is Term of F1(),F2() by A98, A99, Th10;
hence x in F1() -Terms F2() ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F1() -Terms F2() or x in dom f )
assume x in F1() -Terms F2() ; :: thesis: x in dom f
then reconsider x = x as Term of F1(),F2() ;
consider t being Term of F1(),F2(), h being Function such that
A101: ( t = x & h = F . x & S1[t,h] ) by A92;
reconsider h = h as Element of rF by A92, A101, FUNCT_1:def 3;
( x in dom h & dom h in { (dom g) where g is Element of rF : verum } ) by A101, TREES_9:11;
hence x in dom f by A97, TARSKI:def 4; :: thesis: verum
end;
then reconsider f = f as ManySortedSet of F1() -Terms F2() by PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: ( ( for s being SortSymbol of F1()
for x being Element of F2() . s holds f . (root-tree [x,s]) = F3(x,s) ) & ( for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) holds f . ((Sym (o,F2())) -tree p) = F4(o,(f * p)) ) )
hereby :: thesis: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) holds f . ((Sym (o,F2())) -tree p) = F4(o,(f * p))
let s be SortSymbol of F1(); :: thesis: for x being Element of F2() . s holds f . (root-tree [x,s]) = F3(x,s)
let x be Element of F2() . s; :: thesis: f . (root-tree [x,s]) = F3(x,s)
reconsider t = root-tree [x,s] as Term of F1(),F2() by MSATERM:4;
S3[t,F . t] by A92;
then consider g being Function such that
A102: ( g = F . t & S1[t,g] ) ;
g in rF by A92, A102, FUNCT_1:def 3;
then A103: g c= f by ZFMISC_1:74;
t in dom g by A102, TREES_9:11;
hence f . (root-tree [x,s]) = g . t by A103, FOMODEL0:51
.= F3(x,s) by A102, TREES_9:11 ;
:: thesis: verum
end;
let o be OperSymbol of F1(); :: thesis: for p being ArgumentSeq of Sym (o,F2()) holds f . ((Sym (o,F2())) -tree p) = F4(o,(f * p))
let p be ArgumentSeq of Sym (o,F2()); :: thesis: f . ((Sym (o,F2())) -tree p) = F4(o,(f * p))
reconsider t = (Sym (o,F2())) -tree p as Term of F1(),F2() ;
S3[t,F . t] by A92;
then consider g being Function such that
A104: ( g = F . t & S1[t,g] ) ;
A105: g in rF by A92, A104, FUNCT_1:def 3;
then A106: g c= f by ZFMISC_1:74;
A107: t in dom g by A104, TREES_9:11;
( rng p c= Subtrees t & (rng p) /\ (dom f) c= rng p ) by Th11, XBOOLE_1:17;
then (rng p) /\ (dom f) c= dom g by A104;
then A108: g * p = f * p by A105, ZFMISC_1:74, ALGSPEC1:2;
thus f . ((Sym (o,F2())) -tree p) = g . t by A106, A107, FOMODEL0:51
.= F4(o,(f * p)) by A104, TREES_9:11, A108 ; :: thesis: verum