let I, J be set ; :: 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 p being Element of Args (o,(Free (S,X))) st J = [o, the carrier of S] holds
(o -term p) " I = (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )
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 p being Element of Args (o,(Free (S,X))) st J = [o, the carrier of S] holds
(o -term p) " I = (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )
let o be OperSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st J = [o, the carrier of S] holds
(o -term p) " I = (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st J = [o, the carrier of S] holds
(o -term p) " I = (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )
let p be Element of Args (o,(Free (S,X))); :: thesis: ( J = [o, the carrier of S] implies (o -term p) " I = (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) )
set X = { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ;
assume A0: J = [o, the carrier of S] ; :: thesis: (o -term p) " I = (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )
dom (doms p) = dom p by FUNCT_6:def 2;
then A4: len (doms p) = len p by FINSEQ_3:29;
thus (o -term p) " I c= (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) :: according to XBOOLE_0:def 10 :: thesis: (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) c= (o -term p) " I

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (o -term p) " I or x in (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) )
assume x in (o -term p) " I ; :: thesis: x in (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )
then A1: ( x in dom (o -term p) & (o -term p) . x in I ) by FUNCT_1:def 7;
then x in tree (doms p) by TREES_4:10;

per cases then ( x = {} or ex i being Nat ex q being FinSequence st
( i < len (doms p) & q in (doms p) . (i + 1) & x = <*i*> ^ q ) ) by TREES_3:def 15;

suppose x = {} ; :: thesis: x in (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )

then ( (o -term p) . x = J & x in {{}} ) by A0, TARSKI:def 1, TREES_4:def 4;
then x in IFIN (J,I,{{}},{}) by A1, MATRIX_7:def 1;
hence x in (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex i being Nat ex q being FinSequence st
( i < len (doms p) & q in (doms p) . (i + 1) & x = <*i*> ^ q ) ; :: thesis: x in (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )

then consider i being Nat, q being FinSequence such that
A2: ( i < len (doms p) & q in (doms p) . (i + 1) & x = <*i*> ^ q ) ;
( 1 <= i + 1 & i + 1 <= len p ) by A4, A2, NAT_1:11, NAT_1:13;
then A5: i + 1 in dom p by FINSEQ_3:25;
then reconsider px = p . (i + 1) as DecoratedTree by TREES_3:24;
A6: dom px = (doms p) . (i + 1) by A5, FUNCT_6:def 2;
then (o -term p) . x = px . q by A2, A4, TREES_4:12;
then q in px " I by A1, A2, A6, FUNCT_1:def 7;
then ( <*i*> ^ q in <*i*> ^^ (px " I) & <*i*> ^^ (px " I) in { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) by A2, A4;
then x in union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } by A2, TARSKI:def 4;
hence x in (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) or x in (o -term p) " I )
assume x in (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) ; :: thesis: x in (o -term p) " I

per cases then ( x in IFIN (J,I,{{}},{}) or x in union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) by XBOOLE_0:def 3;

suppose x in IFIN (J,I,{{}},{}) ; :: thesis: x in (o -term p) " I

then ( ( J in I & x in {{}} ) or ( J nin I & x in {} ) ) by MATRIX_7:def 1;
then ( x = {} & J in I & (o -term p) . {} = J & {} in dom (o -term p) ) by A0, TREES_1:22, TREES_4:def 4;
hence x in (o -term p) " I by FUNCT_1:def 7; :: thesis: verum

end;

suppose x in union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ; :: thesis: x in (o -term p) " I

then consider Y being set such that
A7: ( x in Y & Y in { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } ) by TARSKI:def 4;
consider i being Nat such that
A8: ( Y = <*i*> ^^ ((p . (i + 1)) " I) & i < len p ) by A7;
consider q being Element of (p . (i + 1)) " I such that
A9: ( x = <*i*> ^ q & q in (p . (i + 1)) " I ) by A7, A8;
( 1 <= i + 1 & i + 1 <= len p ) by A8, NAT_1:11, NAT_1:13;
then AA: i + 1 in dom p by FINSEQ_3:25;
then reconsider px = p . (i + 1) as DecoratedTree by TREES_3:24;
( q in dom px & dom px = (doms p) . (i + 1) & dom (o -term p) = tree (doms p) ) by AA, A9, FUNCT_1:def 7, FUNCT_6:def 2, TREES_4:10;
then ( (o -term p) . x = px . q & px . q in I & x in dom (o -term p) ) by A4, A8, A9, FUNCT_1:def 7, TREES_3:def 15, TREES_4:12;
hence x in (o -term p) " I by FUNCT_1:def 7; :: thesis: verum

end;

end;