let S be non empty non void ManySortedSign ; for V being V5() ManySortedSet of the carrier of S
for X1, X2 being non empty Subset of (S -Terms V) holds
( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) )
let V be V5() ManySortedSet of the carrier of S; for X1, X2 being non empty Subset of (S -Terms V) holds
( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) )
let t1, t2 be non empty Subset of (S -Terms V); ( the Arity of (t1 -CircuitStr) tolerates the Arity of (t2 -CircuitStr) & the ResultSort of (t1 -CircuitStr) tolerates the ResultSort of (t2 -CircuitStr) )
set C = [: the carrier' of S,{ the carrier of S}:];
A1:
dom ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t1) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t1
by FUNCT_2:def 1;
A2:
dom (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees t1)) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t1
by RELAT_1:45;
A3:
dom ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t2) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t2
by FUNCT_2:def 1;
A4:
dom (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees t2)) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t2
by RELAT_1:45;
hereby PARTFUN1:def 4 the ResultSort of (t1 -CircuitStr) tolerates the ResultSort of (t2 -CircuitStr)
let x be
set ;
( x in (dom the Arity of (t1 -CircuitStr)) /\ (dom the Arity of (t2 -CircuitStr)) implies the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . x )assume A5:
x in (dom the Arity of (t1 -CircuitStr)) /\ (dom the Arity of (t2 -CircuitStr))
;
the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . xthen A6:
x in dom the
Arity of
(t1 -CircuitStr)
by XBOOLE_0:def 4;
A7:
x in dom the
Arity of
(t2 -CircuitStr)
by A5, XBOOLE_0:def 4;
reconsider u =
x as
Element of
Subtrees t1 by A1, A6;
([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t1) . x in (Subtrees t1) *
by A1, A6, FUNCT_2:5;
then reconsider y1 = the
Arity of
(t1 -CircuitStr) . x as
FinSequence of
Subtrees t1 by FINSEQ_1:def 11;
the
Arity of
(t2 -CircuitStr) . x in (Subtrees t2) *
by A3, A7, FUNCT_2:5;
then reconsider y2 = the
Arity of
(t2 -CircuitStr) . x as
FinSequence of
Subtrees t2 by FINSEQ_1:def 11;
A8:
( ( for
t being
Element of
t1 holds
t is
finite ) & ( for
t being
Element of
t2 holds
t is
finite ) )
;
then A9:
u = (u . {}) -tree y1
by A1, A6, TREES_9:def 13;
u = (u . {}) -tree y2
by A3, A7, A8, TREES_9:def 13;
hence
the
Arity of
(t1 -CircuitStr) . x = the
Arity of
(t2 -CircuitStr) . x
by A9, TREES_4:15;
verum
end;
let x be set ; PARTFUN1:def 4 ( not x in (proj1 the ResultSort of (t1 -CircuitStr)) /\ (proj1 the ResultSort of (t2 -CircuitStr)) or the ResultSort of (t1 -CircuitStr) . x = the ResultSort of (t2 -CircuitStr) . x )
assume A10:
x in (dom the ResultSort of (t1 -CircuitStr)) /\ (dom the ResultSort of (t2 -CircuitStr))
; the ResultSort of (t1 -CircuitStr) . x = the ResultSort of (t2 -CircuitStr) . x
then A11:
x in dom the ResultSort of (t1 -CircuitStr)
by XBOOLE_0:def 4;
A12:
x in dom the ResultSort of (t2 -CircuitStr)
by A10, XBOOLE_0:def 4;
thus the ResultSort of (t1 -CircuitStr) . x =
x
by A2, A11, FUNCT_1:18
.=
the ResultSort of (t2 -CircuitStr) . x
by A4, A12, FUNCT_1:18
; verum