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 ;
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 ;
A7: g . x = (proj (f,x)) . z by
.= h . x by ;
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 ;
hence g . s = h . s by A7; :: thesis: verum
end;
hence y = z by ; :: thesis: verum
end;
hence proj (f,x) is one-to-one by FUNCT_1:def 4; :: thesis: verum