let f be trivial Function; :: thesis: for x being object st x in dom f holds
proj (f,x) is one-to-one
let x be object ; :: thesis: ( x in dom f implies proj (f,x) is one-to-one )
assume A1: x in dom f ; :: thesis: proj (f,x) is one-to-one
then consider t being object such that
A2: dom f = {t} by ZFMISC_1:131;
A3: dom f = {x} by A1, A2, TARSKI:def 1;
set F = proj (f,x);
for y, z being object st y in dom (proj (f,x)) & z in dom (proj (f,x)) & (proj (f,x)) . y = (proj (f,x)) . z holds
y = z
proof
let y, z be object ; :: thesis: ( y in dom (proj (f,x)) & z in dom (proj (f,x)) & (proj (f,x)) . y = (proj (f,x)) . z implies y = z )
assume A4: ( y in dom (proj (f,x)) & z in dom (proj (f,x)) & (proj (f,x)) . y = (proj (f,x)) . z ) ; :: thesis: y = z
then consider g being Function such that
A5: ( y = g & dom g = dom f ) and
for s being object st s in dom f holds
g . s in f . s by CARD_3:def 5;
consider h being Function such that
A6: ( z = h & dom h = dom f ) and
for s being object st s in dom f holds
h . s in f . s by A4, CARD_3:def 5;
A7: g . x = (proj (f,x)) . z by A4, A5, CARD_3:def 16
.= h . x by A4, A6, CARD_3:def 16 ;
for s being object st s in dom g holds
g . s = h . s
proof
let s be object ; :: thesis: ( s in dom g implies g . s = h . s )
assume s in dom g ; :: thesis: g . s = h . s
then s = x by A3, A5, TARSKI:def 1;
hence g . s = h . s by A7; :: thesis: verum
end;
hence y = z by A5, A6, FUNCT_1:2; :: thesis: verum
end;
hence proj (f,x) is one-to-one by FUNCT_1:def 4; :: thesis: verum