let C be initialized ConstructorSignature; for f being one-to-one irrelevant valuation of C ex g being one-to-one irrelevant valuation of C st
for x, y being variable holds
( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )
let f be one-to-one irrelevant valuation of C; ex g being one-to-one irrelevant valuation of C st
for x, y being variable holds
( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )
set Y = { x where x is variable : x -term C in rng f } ;
defpred S1[ object , object ] means ex x being set st
( x in dom f & f . x = root-tree [$1,a_Term] & $2 = root-tree [x,a_Term] );
A1:
for x being object st x in { x where x is variable : x -term C in rng f } holds
ex y being object st S1[x,y]
consider g being Function such that
A5:
dom g = { x where x is variable : x -term C in rng f }
and
A6:
for y being object st y in { x where x is variable : x -term C in rng f } holds
S1[y,g . y]
from CLASSES1:sch 1(A1);
A7:
{ x where x is variable : x -term C in rng f } c= Vars
rng g c= QuasiTerms C
then reconsider g = g as valuation of C by A5, A7, RELSET_1:4;
A12:
g is irrelevant
g is one-to-one
proof
let z1,
z2 be
object ;
FUNCT_1:def 4 ( not z1 in proj1 g or not z2 in proj1 g or not g . z1 = g . z2 or z1 = z2 )
assume that A15:
z1 in dom g
and A16:
z2 in dom g
and A17:
g . z1 = g . z2
;
z1 = z2
reconsider z1 =
z1,
z2 =
z2 as
variable by A15, A16;
consider x1 being
set such that A18:
x1 in dom f
and A19:
f . x1 = z1 -term C
and A20:
g . z1 = root-tree [x1,a_Term]
by A5, A6, A15;
consider x2 being
set such that A21:
x2 in dom f
and A22:
f . x2 = z2 -term C
and A23:
g . z1 = root-tree [x2,a_Term]
by A5, A6, A16, A17;
reconsider x1 =
x1,
x2 =
x2 as
variable by A18, A21;
x1 -term C = x2 -term C
by A20, A23;
then
x1 = x2
by Th50;
hence
z1 = z2
by A19, A22, Th50;
verum
end;
then reconsider g = g as one-to-one irrelevant valuation of C by A12;
take
g
; for x, y being variable holds
( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )
let x, y be variable; ( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )
assume that
A26:
y in dom g
and
A27:
g . y = x -term C
; ( x in dom f & f . x = y -term C )
consider z being set such that
A28:
z in dom f
and
A29:
f . z = root-tree [y,a_Term]
and
A30:
x -term C = root-tree [z,a_Term]
by A5, A6, A26, A27;
reconsider z = z as variable by A28;
x -term C = z -term C
by A30;
hence
( x in dom f & f . x = y -term C )
by A28, A29, Th50; verum