defpred S1[ object ] means F5() . $1 = F6() . $1;
A5: for s being SortSymbol of F1()
for x being Element of F2() . s holds S1[ root-tree [x,s]]
proof
let s be SortSymbol of F1(); :: thesis: for x being Element of F2() . s holds S1[ root-tree [x,s]]
let x be Element of F2() . s; :: thesis: S1[ root-tree [x,s]]
thus F5() . (root-tree [x,s]) = F3(x,s) by A1
.= F6() . (root-tree [x,s]) by A3 ; :: thesis: verum
end;
A6: 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
S1[t] ) holds
S1[[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
S1[t] ) holds
S1[[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
S1[t] ) implies S1[[o, the carrier of F1()] -tree p] )
assume A7: for t being Term of F1(),F2() st t in rng p holds
S1[t] ; :: thesis: S1[[o, the carrier of F1()] -tree p]
A8: ( dom (F5() * p) = dom p & dom (F6() * p) = dom p ) by PARTFUN1:def 2;
now :: thesis: for x being object st x in dom p holds
(F5() * p) . x = (F6() * p) . x
let x be object ; :: thesis: ( x in dom p implies (F5() * p) . x = (F6() * p) . x )
assume A9: x in dom p ; :: thesis: (F5() * p) . x = (F6() * p) . x
then reconsider i = x as Element of NAT ;
reconsider t = p . i as Term of F1(),F2() by A9, MSATERM:22;
t in rng p by A9, FUNCT_1:def 3;
then S1[t] by A7;
hence (F5() * p) . x = F6() . t by A9, FUNCT_1:13
.= (F6() * p) . x by A9, FUNCT_1:13 ;
:: thesis: verum
end;
then F5() * p = F6() * p by A8;
hence F5() . ([o, the carrier of F1()] -tree p) = F4(o,(F6() * p)) by A2
.= F6() . ([o, the carrier of F1()] -tree p) by A4 ;
:: thesis: verum
end;
A10: for t being Term of F1(),F2() holds S1[t] from MSATERM:sch 1(A5, A6);
 for x being object st x in F1() -Terms F2() holds
S1[x] by A10;
hence F5() = F6() ; :: thesis: verum